Dr Michael Tautschnig

Lecturer
Email: michael.tautschnig@qmul.ac.ukTelephone: +44 20 7882 5226Room Number: Peter Landin, CS 432Website: http://www.tautschnig.netOffice Hours: Tuesday 13:00-14:30
Teaching
Programming for Artificial Intelligence and Data Science (Postgraduate)
This module provides an intensive practical introduction to programming in Python, suitable for students with some degree of mathematical or statistical maturity. It covers a range of practical skills and underlying knowledge. These include the basic programming constructs for control, data structuring and modularisation; the use of systems for collaborative development and version control such as Git; unit testing and documentation; project structures and continuous integration/deployment.
Research
Research Interests:
Software VerificationConcurrency
Decision Procedures
Publications
- Chong N, Cook B, Eidelman J et al. (2021), Code-level model checking in the software development workflow at Amazon Web Services $nameOfConferenceDOI: 10.1002/spe.2949
- Cook B, Döbel B, Kroening D et al. (2020), Using model checking tools to triage the severity of security bugs in the Xen hypervisor Formal Methods in Computer Aided Design
- Chong N, Cook B, Kallas K et al. (2020), Code-level model checking in the software development workflow $nameOfConference
- Beyer D, Dangl M, Lemberger T et al. (2019), Tests from Witnesses Execution-Based Validation of Verification Results Tests and Proofs
- Khazem K, Tautschnig M (2019), CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker $nameOfConference
- Khazem K, Tautschnig M (2019), CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution) $nameOfConference
- Cook B, Khazem K, Kroening D et al. (2018), Model Checking Boot Code from AWS Data Centers Computer Aided Verification
- Beyer D, Dangl M, Lemberger T et al. (2018), Tests from Witnesses $nameOfConference
- Liang L, Melham T, Kroening D et al. (2018), Effective verification for low-level software with competing interrupts $nameOfConferenceDOI: 10.1145/3147432
- Huisman M, Klebanov V, Monahan R et al. (2017), VerifyThis 2015 A program verification competition $nameOfConference
- Prabhu S, Schrammel P, Srivas M et al. (2017), Concurrent Program Verification with Invariant-Guided Underapproximation Automated Technology for Verification and Analysis
- MALACARIA P, TAUTCHNING M, DISTEFANO D (2016), Information leakage analysis of complex C code and its application to OpenSSL 7th International Symposium on Leveraging Applications
- Nellis A, Kesseli P, Conmy PR et al. (2016), Assisted Coverage Closure $nameOfConference
- Khazem K, Tautschnig M (2016), smid: A Black-Box Program Driver $nameOfConference
- Nellis A, Kesseli P, Conmy PR et al. (2016), Assisted Coverage Closure. $nameOfConference
- Mukherjee R, Tautschnig M, Kroening D (2016), V2c – A Verilog to C translator $nameOfConference
- Khazem K, Tautschnig M (2016), smid: A Black-Box Program Driver $nameOfConference
- Mukherjee R, Tautschnig M, Kroening D (2016), v2c - A Verilog to C Translator Tools and Algorithms for the Construction and Analysis of Systems
- Holzer A, Schallhart C, Tautschnig M et al. (2015), Closure properties and complexity of rational sets of regular languages $nameOfConference
- Kroening D, Liang L, Melham T et al. (2015), Effective verification of low-level software with nested interrupts $nameOfConference
- Tautschnig M (2015), CBMC: Bounded model checking of concurrent C programs $nameOfConference
- Chapman M, Chockler H, Kesseli P et al. (2015), Learning the language of error $nameOfConference
- Bloem R, Koenighofer R, Rock F et al. (2014), Automating test-suite augmentation $nameOfConferenceDOI: 10.1109/QSIC.2014.40
- Alglave J, Maranget L, Tautschnig M (2014), Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. $nameOfConferenceDOI: 10.1145/2627752
- Kroening D, Tautschnig M (2014), Automating software analysis at large scale $nameOfConference
- Kroening D, Tautschnig M (2014), CBMC - C Bounded Model Checker (Competition contribution) $nameOfConference
- Kroening D, Tautschnig M (2014), CBMC – C Bounded Model Checker $nameOfConference
- Alglave J, Maranget L, Tautschnig M (2014), Herding cats: Modelling, simulation, testing, and data mining for weak memory $nameOfConferenceDOI: 10.1145/2627752
- Alglave J, Maranget L, Tautschnig M (2014), Herding cats: Modelling, simulation, testing, and data-mining for weak memory $nameOfConference
- Beyer D, Holzer A, Tautschnig M et al. (2014), Reusing information in multi-goal reachability analyses $nameOfConference
- Holzer A, Schallhart C, Tautschnig M et al. (2013), On the structure and complexity of rational sets of regular languages $nameOfConference
- Alglave J, Kroening D, Nimal V et al. (2013), Software verification for weak memory via program transformation $nameOfConference
- Horn A, Tautschnig M, Val C et al. (2013), Formal co-validation of low-level hardware/software interfaces $nameOfConference
- Alglave J, Maranget L, Tautschnig M (2013), Herding Cats. $nameOfConference
- Beyer D, Holzer A, Tautschnig M et al. (2013), Information Reuse for Multi-goal Reachability Analyses. $nameOfConference
- Holzer A, Schallhart C, Tautschnig M et al. (2013), On the Structure and Complexity of Rational Sets of Regular Languages. $nameOfConference
- Chockler H, Denaro G, Ling M et al. (2013), PINCETTE - Validating Changes and Upgrades in Networked Software. $nameOfConferenceDOI: 10.1109/CSMR.2013.72
- Alglave J, Kroening D, Tautschnig M (2013), Partial Orders for Efficient BMC of Concurrent Software $nameOfConference
- Alglave J, Kroening D, Tautschnig M (2013), Partial Orders for Efficient Bounded Model Checking of Concurrent Software. $nameOfConference
- Alglave J, Kroening D, Nimal V et al. (2013), Software Verification for Weak Memory via Program Transformation. $nameOfConference
- Donaldson AF, Kaiser A, Kroening D et al. (2012), Counterexample-guided abstraction refinement for symmetric concurrent programs. $nameOfConference
- D'Silva V, Haller L, Kroening D et al. (2012), Numeric Bounds Analysis with Conflict-Driven Learning. $nameOfConference
- Holzer A, Kroening D, Schallhart C et al. (2012), Proving Reachability Using FShell $nameOfConference
- Holzer A, Kroening D, Schallhart C et al. (2012), Proving Reachability Using FShell - (Competition Contribution). $nameOfConference
- Basler G, Donaldson A, Kaiser A et al. (2012), satabs: A Bit-Precise Verifier for C Programs $nameOfConference
- Basler G, Donaldson AF, Kaiser A et al. (2012), satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). $nameOfConference
- Bünte S, Zolda M, Tautschnig M et al. (2011), Improving the Confidence in Measurement-Based Timing Analysis. $nameOfConference
- Alglave J, Donaldson AF, Kroening D et al. (2011), Making Software Verification Tools Really Work. $nameOfConference
- Holzer A, Januzaj V, Kugele S et al. (2011), Seamless Testing for Models and Code. $nameOfConference
- Alglave J, Kroening D, Lugton J et al. (2011), Soundness of Data Flow Analyses for Weak Memory Models. $nameOfConference
- Holzer A, Tautschnig M, Schallhart C et al. (2010), An Introduction to Test Specification in FQL. $nameOfConference
- Bauer A, Leucker M, Schallhart C et al. (2010), Don't care in SMT: building flexible yet efficient abstraction/refinement solvers. $nameOfConference
- Holzer A, Schallhart C, Tautschnig M et al. (2010), How did you specify your test suite. $nameOfConference
- Haberl W, Herrmannsdoerfer M, Kugele S et al. (2010), Seamless Model-Driven Development Put into Practice. $nameOfConference
- Holzer A, Januzaj V, Kugele S et al. (2010), Timely Time Estimates. $nameOfConference
- Langer B, Tautschnig M (2009), Navigating the Requirements Jungle $nameOfConference
- Kugele S, Haberl W, Tautschnig M et al. (2009), Optimizing Automatic Deployment Using Non-functional Requirement Annotations $nameOfConference
- Haberl W, Tautschnig M, Baumgarten U (2009), Generating distributed code from cola models $nameOfConference
- Holzer A, Schallhart C, Tautschnig M et al. (2009), Query-Driven Program Testing. $nameOfConference
- Gruber H, Holzer M, Tautschnig M (2009), Short Regular Expressions from Finite Automata: Empirical Results. $nameOfConference
- Bünte S, Tautschnig M (2008), A Benchmarking Suite for Measurement-Based WCET Analysis Tools. $nameOfConferenceDOI: 10.1109/ICSTW.2008.1
- Wang Z, Herkersdorf A, Merenda S et al. (2008), A Model Driven Development Approach for Implementing Reactive Systems in Hardware $nameOfConference
- Wang Z, Herkersdorf A, Merenda S et al. (2008), A Model Driven Development Approach for Implementing Reactive Systems in Hardware. $nameOfConference
- Wang Z, Haberl W, Kugele S et al. (2008), Automatic generation of systemc models from component-based designs for early design validation and performance analysis. $nameOfConference
- Holzer A, Schallhart C, Tautschnig M et al. (2008), FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. $nameOfConference
- Langer B, Tautschnig M (2008), Navigating the Requirements Jungle. $nameOfConference
- Kugele S, Haberl W, Tautschnig M et al. (2008), Optimizing Automatic Deployment Using Non-functional Requirement Annotations. $nameOfConference
- Haberl W, Tautschnig M, Baumgarten U et al. (2008), Running COLA on embedded systems $nameOfConference
- Kühnel C, Bauer A, Tautschnig M (2007), Compatibility and reuse in component-based systems via type and unit inference. $nameOfConference
- Bauer A, Leucker M, Schallhart C et al. (2007), Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers. $nameOfConference
- Bauer A, Pister M, Tautschnig M (2007), Tool-support for the analysis of hybrid systems and models. $nameOfConference