Dr Michael Tautschnig
Lecturer
School of Electronic Engineering and Computer Science
Queen Mary University of London
Queen Mary University of London
Research
Software Verification, Concurrency, Decision Procedures
Publications
Publications of specific relevance to the Centre for Fundamental Computer Science2024
2022
Beyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T and Tautschnig M (2022). Verification Witnesses. ACM Transactions on Software Engineering and Methodology, Association for Computing Machinery (ACM) vol. 31 (4) 08-09-2022
Beyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T and Tautschnig M (2022). Verification Witnesses. ACM Trans. Softw. Eng. Methodol. vol. 31, 57:1-57:1. 01-01-2022
2021
Chong N, Cook B, Eidelman J, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M and Tuttle MR (2021). Code-level model checking in the software development workflow at Amazon Web Services. Software - Practice and Experience vol. 51 (4), 772-797. 01-04-2021
2020
Cook B, Döbel B, Kroening D, Manthey N, Pohlack M, Polgreen E, Tautschnig M and Wieczorkiewicz P (2020). Using model checking tools to triage the severity of security bugs in the Xen hypervisor. Formal Methods in Computer Aided Design. 24-09-2020
Chong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M and Tuttle MR (2020). Code-level model checking in the software development workflow. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice. 27-06-2020
2019
Beyer D, Dangl M, Lemberger T and Tautschnig M (2019). Tests from Witnesses Execution-Based Validation of Verification Results. Tests and Proofs. 05-07-2019
Khazem K and Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution). 01-01-2019
Khazem K and Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker. Tools and Algorithms for the Construction and Analysis of Systems 199-203. 01-01-2019
2018
Cook B, Khazem K, Kroening D, Tasiran S, TAUTSCHNIG M and Tuttle M (2018). Model Checking Boot Code from AWS Data Centers. Computer Aided Verification. 18-07-2018
Liang L, Melham T, Kroening D, Schrammel P and TAUTSCHNIG M (2018). Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems, Association for Computing Machinery vol. 17, 1-26. 02-01-2018
Beyer D, Dangl M, Lemberger T and Tautschnig M (2018). Tests from Witnesses. Tests and Proofs 3-23. 01-01-2018
2017
Huisman M, Klebanov V, Monahan R and Tautschnig M (2017). VerifyThis 2015 A program verification competition. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER vol. 19 (6), 763-771. 19-10-2017
Prabhu S, Schrammel P, Srivas M, Tautschnig M and Yeolekar A (2017). Concurrent Program Verification with Invariant-Guided Underapproximation. Automated Technology for Verification and Analysis. 27-09-2017
2016
MALACARIA P, TAUTCHNING M and DISTEFANO D (2016). Information leakage analysis of complex C code and its application to OpenSSL. 7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016. 05-10-2016
Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M (2016). Assisted Coverage Closure. NASA Formal Methods vol. 9690, 49-64. 04-06-2016
Mukherjee R, Tautschnig M and Kroening D (2016). v2c - A Verilog to C Translator. Tools and Algorithms for the Construction and Analysis of Systems. 01-01-2016
Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M (2016). Assisted Coverage Closure., Editors: Rayadurgam S and Tkachuk O. 01-01-2016
2015
Holzer A, Schallhart C, Tautschnig M and Veith H (2015). Closure properties and complexity of rational sets of regular languages. Theoretical Computer Science, Elsevier vol. 605, 62-79. 01-11-2015
Kroening D, Liang L, Melham T, Schrammel P and Tautschnig M (2015). Effective verification of low-level software with nested interrupts. Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015. 22-04-2015
Chapman M, Chockler H, Kesseli P, Kroening D, Strichman O and Tautschnig M (2015). Learning the Language of Error. 01-01-2015
2014
Bloem R, Konighofer R, Rock F and Tautschnig M (2014). Automating test-suite augmentation. 2014 14th International Conference on Quality Software. 01-10-2014
Alglave J, Maranget L and Tautschnig M (2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Transactions on Programming Languages and Systems, Association for Computing Machinery vol. 36 (2), 1-74. 01-07-2014
Kroening D and Tautschnig M (2014). CBMC - C Bounded Model Checker (Competition contribution). 01-01-2014
Beyer D, Holzer A, Tautschnig M and Veith H (2014). Reusing information in multi-goal reachability analyses. 01-01-2014
Alglave J, Maranget L, Tautschnig M and ACM (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. 01-01-2014
Kroening D and Tautschnig M (2014). CBMC – C Bounded Model Checker. Tools and Algorithms for the Construction and Analysis of Systems 389-391. 01-01-2014
2013
Horn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J and Kroening D (2013). Formal co-validation of low-level hardware/software interfaces. 2013 Formal Methods in Computer-Aided Design. 06-12-2013
Alglave J, Maranget L and Tautschnig M (2013). Herding Cats - Modelling, simulation, testing, and data-mining for weak
memory. 30-08-2013
Holzer A, Schallhart C, Tautschnig M and Veith H (2013). On the Structure and Complexity of Rational Sets of Regular Languages. 26-05-2013
Alglave J, Kroening D and Tautschnig M (2013). Partial Orders for Efficient BMC of Concurrent Software. 08-01-2013
Beyer D, Holzer A, Tautschnig M and Veith H (2013). Information Reuse for Multi-goal Reachability Analyses., Editors: Felleisen M and Gardner P. 01-01-2013
Alglave J, Kroening D, Nimal V and Tautschnig M (2013). Software Verification for Weak Memory via Program Transformation., Editors: Felleisen M and Gardner P. 01-01-2013
Chockler H, Denaro G, Ling M, Fedyukovich G, Hyvärinen AEJ, Mariani L, Muhammad A, Oriol M, Rajan A, Sery O, Sharygina N and Tautschnig M (2013). PINCETTE - Validating Changes and Upgrades in Networked Software., Editors: Cleve A, Ricca F and Cerioli M. 01-01-2013
Alglave J, Kroening D and Tautschnig M (2013). Partial Orders for Efficient Bounded Model Checking of Concurrent Software., Editors: Sharygina N and Veith H. 01-01-2013
Holzer A, Schallhart C, Tautschnig M and Veith H (2013). On the Structure and Complexity of Rational Sets of Regular Languages., Editors: Seth A and Vishnoi NK. 01-01-2013
2012
Alglave J, Kroening D, Nimal V and Tautschnig M (2012). Software Verification for Weak Memory via Program Transformation. 30-07-2012
D'Silva VV, Haller L, Kroening D and Tautschnig M (2012). Numeric Bounds Analysis with Conflict-Driven Learning., Editors: Flanagan C and König B. 01-01-2012
Donaldson AF, Kaiser A, Kroening D, Tautschnig M and Wahl T (2012). Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. vol. 41, 25-44. 01-01-2012
Holzer A, Kroening D, Schallhart C, Tautschnig M and Veith H (2012). Proving Reachability Using FShell - (Competition Contribution)., Editors: Flanagan C and König B. 01-01-2012
Basler G, Donaldson AF, Kaiser A, Kroening D, Tautschnig M and Wahl T (2012). satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution)., Editors: Flanagan C and König B. 01-01-2012
Holzer A, Kroening D, Schallhart C, Tautschnig M and Veith H (2012). Proving Reachability Using FShell. Tools and Algorithms for the Construction and Analysis of Systems 538-541. 01-01-2012
Basler G, Donaldson A, Kaiser A, Kroening D, Tautschnig M and Wahl T (2012). satabs: A Bit-Precise Verifier for C Programs. Tools and Algorithms for the Construction and Analysis of Systems 552-555. 01-01-2012
2011
Holzer A, Januzaj V, Kugele S, Langer B, Schallhart C, Tautschnig M and Veith H (2011). Seamless Testing for Models and Code., Editors: Giannakopoulou D and Orejas F. 01-01-2011
Bünte S, Zolda M, Tautschnig M and Kirner R (2011). Improving the Confidence in Measurement-Based Timing Analysis. 01-01-2011
Alglave J, Kroening D, Lugton J, Nimal V and Tautschnig M (2011). Soundness of Data Flow Analyses for Weak Memory Models., Editors: Yang H. 01-01-2011
Alglave J, Donaldson AF, Kroening D and Tautschnig M (2011). Making Software Verification Tools Really Work., Editors: Bultan T and Hsiung P-A. 01-01-2011
2010
Haberl W, Herrmannsdoerfer M, Kugele S, Tautschnig M and Wechs M (2010). Seamless Model-Driven Development Put into Practice., Editors: Margaria T and Steffen B. 01-01-2010
Holzer A, Schallhart C, Tautschnig M and Veith H (2010). How did you specify your test suite., Editors: Pecheur C, Andrews J and Nitto ED. 01-01-2010
Holzer A, Tautschnig M, Schallhart C and Veith H (2010). An Introduction to Test Specification in FQL., Editors: Barner S, Harris IG, Kroening D and Raz O. 01-01-2010
Holzer A, Januzaj V, Kugele S and Tautschnig M (2010). Timely Time Estimates., Editors: Margaria T and Steffen B. 01-01-2010
Bauer A, Leucker M, Schallhart C and Tautschnig M (2010). Don't care in SMT: building flexible yet efficient abstraction/refinement solvers. Int. J. Softw. Tools Technol. Transf. vol. 12, 23-37. 01-01-2010
2009
Kugele S, Haberl W, Tautschnig M and Wechs M (2009). Optimizing Automatic Deployment Using Non-functional Requirement Annotations. Communications in Computer and Information Science vol. 17, 400-414. 01-12-2009
Langer B and Tautschnig M (2009). Navigating the Requirements Jungle. Communications in Computer and Information Science vol. 17, 354-368. 01-12-2009
Gruber H, Holzer M and Tautschnig M (2009). Short Regular Expressions from Finite Automata: Empirical Results., Editors: Maneth S. 01-01-2009
Holzer A, Schallhart C, Tautschnig M and Veith H (2009). Query-Driven Program Testing., Editors: Jones ND and Müller-Olm M. 01-01-2009
Haberl W, Tautschnig M and Baumgarten U (2009). Generating Distributed Code from Cola Models. Trends in Communication Technologies and Engineering Science 265-279. 01-01-2009
2008
Langer B and Tautschnig M (2008). Navigating the Requirements Jungle., Editors: Margaria T and Steffen B. 01-01-2008
Holzer A, Schallhart C, Tautschnig M and Veith H (2008). FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement., Editors: Gupta A and Malik S. 01-01-2008
Kugele S, Haberl W, Tautschnig M and Wechs M (2008). Optimizing Automatic Deployment Using Non-functional Requirement Annotations., Editors: Margaria T and Steffen B. 01-01-2008
Wang Z, Haberl W, Kugele S and Tautschnig M (2008). Automatic generation of systemc models from component-based designs for early design validation and performance analysis., Editors: Avritzer A, Weyuker EJ and Woodside CM. 01-01-2008
Wang Z, Herkersdorf A, Merenda S and Tautschnig M (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. 01-01-2008
Bünte S and Tautschnig M (2008). A Benchmarking Suite for Measurement-Based WCET Analysis Tools. 01-01-2008
Wang Z, Herkersdorf A, Merenda S and Tautschnig M (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. 01-01-2008
2007
Bauer A, Pister M and Tautschnig M (2007). Tool-support for the analysis of hybrid systems and models., Editors: Lauwereins R and Madsen J. 01-01-2007
Kühnel C, Bauer A and Tautschnig M (2007). Compatibility and reuse in component-based systems via type and unit inference. 01-01-2007
Bauer A, Leucker M, Schallhart C and Tautschnig M (2007). Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers., Editors: Ameur YA, Boniol F and Wiels V. 01-01-2007