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
Neural Model Checking.Giacobbe M, Kroening D, Pal A and Tautschnig M
CoRR. vol. abs/2410.23790
01-01-2024
2022
Verification WitnessesBeyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T and Tautschnig M
Acm Transactions on Software Engineering and Methodology, Association For Computing Machinery (Acm) vol. 31 (4)
08-09-2022
Verification Witnesses.Beyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T and Tautschnig M
Acm Trans. Softw. Eng. Methodol. vol. 31, 57:1-57:1.
01-01-2022
2021
Code-level model checking in the software development workflow at Amazon Web ServicesChong N, Cook B, Eidelman J, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M and Tuttle MR
Software - Practice and Experience vol. 51 (4), 772-797.
01-04-2021
2020
Using model checking tools to triage the severity of security bugs in the Xen hypervisorCook B, Döbel B, Kroening D, Manthey N, Pohlack M, Polgreen E, Tautschnig M and Wieczorkiewicz P
Formal Methods in Computer Aided Design. vol. 00, 185-193.
24-09-2020
Code-level model checking in the software development workflowChong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M and Tuttle MR
Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice., 11-20.
27-06-2020
2019
Tests from Witnesses Execution-Based Validation of Verification ResultsBeyer D, Dangl M, Lemberger T and Tautschnig M
Tests and Proofs. vol. 10889, 3-23.
05-07-2019
CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution)Khazem K and Tautschnig M
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 11429 LNCS, 199-203.
01-01-2019
CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model CheckerKhazem K and Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 199-203.
01-01-2019
2018
Model Checking Boot Code from AWS Data CentersCook B, Khazem K, Kroening D, Tasiran S, TAUTSCHNIG M and Tuttle M
Computer Aided Verification.
18-07-2018
Effective verification for low-level software with competing interruptsLiang L, Melham T, Kroening D, Schrammel P and TAUTSCHNIG M
Acm Transactions on Embedded Computing Systems, Association For Computing Machinery vol. 17, 1-26.
02-01-2018
Tests from WitnessesBeyer D, Dangl M, Lemberger T and Tautschnig M
In Tests and Proofs, Springer Nature 3-23.
01-01-2018
2017
VerifyThis 2015 A program verification competitionHuisman M, Klebanov V, Monahan R and Tautschnig M
International Journal on Software Tools For Technology Transfer vol. 19 (6), 763-771.
19-10-2017
Concurrent Program Verification with Invariant-Guided UnderapproximationPrabhu S, Schrammel P, Srivas M, Tautschnig M and Yeolekar A
Automated Technology for Verification and Analysis. vol. 10482, 241-248.
27-09-2017
2016
Information leakage analysis of complex C code and its application to OpenSSLMALACARIA P, TAUTCHNING M and DISTEFANO D
7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016.
05-10-2016
Assisted Coverage ClosureNellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M
Nasa Formal Methods vol. 9690, 49-64.
04-06-2016
v2c – A Verilog to C TranslatorMukherjee R, Tautschnig M and Kroening D
Lecture Notes in Computer Science. vol. 9636, 580-586.
01-01-2016
smid: A Black-Box Program DriverKhazem K and Tautschnig M
Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings., 182-188.
01-01-2016
v2c - A Verilog to C TranslatorMukherjee R, Tautschnig M and Kroening D
Tools and Algorithms for the Construction and Analysis of Systems., 580-586.
01-01-2016
Assisted Coverage Closure.Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M
NFM. vol. 9690, 49-64. Editors: Rayadurgam S and Tkachuk O.
01-01-2016
2015
Closure properties and complexity of rational sets of regular languagesHolzer A, Schallhart C, Tautschnig M and Veith H
Theoretical Computer Science, Elsevier vol. 605, 62-79.
01-11-2015
Effective verification of low-level software with nested interruptsKroening D, Liang L, Melham T, Schrammel P and Tautschnig M
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015., 229-234.
22-04-2015
Learning the Language of ErrorChapman M, Chockler H, Kesseli P, Kroening D, Strichman O and Tautschnig M
Lecture Notes in Computer Science. vol. 9364, 114-130.
01-01-2015
CBMC: Bounded model checking of concurrent C programsTautschnig M
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9232, 11-12.
01-01-2015
2014
Automating test-suite augmentationBloem R, Konighofer R, Rock F and Tautschnig M
2014 14th International Conference on Quality Software., 67-72.
01-10-2014
Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.Alglave J, Maranget L and Tautschnig M
Acm Transactions on Programming Languages and Systems, Association For Computing Machinery vol. 36 (2), 1-74.
01-07-2014
Herding catsAlglave J, Maranget L and Tautschnig M
ACM SIGPLAN Notices. vol. 49 (6), 40-40.
05-06-2014
Automating Software Analysis at Large ScaleKroening D and Tautschnig M
Lecture Notes in Computer Science. vol. 8934, 30-39.
01-01-2014
CBMC - C Bounded Model Checker (Competition contribution)Kroening D and Tautschnig M
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 8413 LNCS, 389-391.
01-01-2014
Reusing information in multi-goal reachability analysesBeyer D, Holzer A, Tautschnig M and Veith H
Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI). vol. P227, 97-98.
01-01-2014
Herding cats: Modelling, simulation, testing, and data-mining for weak memoryAlglave J, Maranget L, Tautschnig M and ACM
PLDI'14: PROCEEDINGS OF THE 2014 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION., 40-40.
01-01-2014
CBMC – C Bounded Model CheckerKroening D and Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 389-391.
01-01-2014
2013
Formal co-validation of low-level hardware/software interfacesHorn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J and Kroening D
2013 Formal Methods in Computer-Aided Design., 121-128.
06-12-2013
Herding Cats - Modelling, simulation, testing, and data-mining for weak
memoryAlglave J, Maranget L and Tautschnig M
30-08-2013
On the Structure and Complexity of Rational Sets of Regular LanguagesHolzer A, Schallhart C, Tautschnig M and Veith H
26-05-2013
Partial Orders for Efficient BMC of Concurrent SoftwareAlglave J, Kroening D and Tautschnig M
08-01-2013
Information Reuse for Multi-goal Reachability Analyses.Beyer D, Holzer A, Tautschnig M and Veith H
ESOP. vol. 7792, 472-491. Editors: Felleisen M and Gardner P.
01-01-2013
Software Verification for Weak Memory via Program Transformation.Alglave J, Kroening D, Nimal V and Tautschnig M
Proceedings of 22nd European Symposium on Programming. vol. 7792, 512-532. Editors: Felleisen M and Gardner P.
01-01-2013
PINCETTE - Validating Changes and Upgrades in Networked Software.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
CSMR., 461-464. Editors: Cleve A, Ricca F and Cerioli M.
01-01-2013
Partial Orders for Efficient Bounded Model Checking of Concurrent Software.Alglave J, Kroening D and Tautschnig M
CAV. vol. 8044, 141-157. Editors: Sharygina N and Veith H.
01-01-2013
On the Structure and Complexity of Rational Sets of Regular Languages.Holzer A, Schallhart C, Tautschnig M and Veith H
FSTTCS. vol. 24, 377-388. Editors: Seth A and Vishnoi NK.
01-01-2013
2012
Software Verification for Weak Memory via Program TransformationAlglave J, Kroening D, Nimal V and Tautschnig M
30-07-2012
Numeric Bounds Analysis with Conflict-Driven Learning.D'Silva VV, Haller L, Kroening D and Tautschnig M
TACAS. vol. 7214, 48-63. Editors: Flanagan C and König B.
01-01-2012
Counterexample-guided abstraction refinement for symmetric concurrent programs.Donaldson AF, Kaiser A, Kroening D, Tautschnig M and Wahl T
Formal Methods Syst. Des. vol. 41, 25-44.
01-01-2012
Proving Reachability Using FShell - (Competition Contribution).Holzer A, Kroening D, Schallhart C, Tautschnig M and Veith H
TACAS. vol. 7214, 538-541. Editors: Flanagan C and König B.
01-01-2012
satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).Basler G, Donaldson AF, Kaiser A, Kroening D, Tautschnig M and Wahl T
TACAS. vol. 7214, 552-555. Editors: Flanagan C and König B.
01-01-2012
Proving Reachability Using FShellHolzer A, Kroening D, Schallhart C, Tautschnig M and Veith H
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 538-541.
01-01-2012
satabs: A Bit-Precise Verifier for C ProgramsBasler G, Donaldson A, Kaiser A, Kroening D, Tautschnig M and Wahl T
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 552-555.
01-01-2012
2011
Seamless Testing for Models and Code.Holzer A, Januzaj V, Kugele S, Langer B, Schallhart C, Tautschnig M and Veith H
FASE. vol. 6603, 278-293. Editors: Giannakopoulou D and Orejas F.
01-01-2011
Improving the Confidence in Measurement-Based Timing Analysis.Bünte S, Zolda M, Tautschnig M and Kirner R
ISORC., 144-151.
01-01-2011
Soundness of Data Flow Analyses for Weak Memory Models.Alglave J, Kroening D, Lugton J, Nimal V and Tautschnig M
APLAS. vol. 7078, 272-288. Editors: Yang H.
01-01-2011
Making Software Verification Tools Really Work.Alglave J, Donaldson AF, Kroening D and Tautschnig M
ATVA. vol. 6996, 28-42. Editors: Bultan T and Hsiung P-A.
01-01-2011
2010
Seamless Model-Driven Development Put into Practice.Haberl W, Herrmannsdoerfer M, Kugele S, Tautschnig M and Wechs M
ISoLA (1). vol. 6415, 18-32. Editors: Margaria T and Steffen B.
01-01-2010
How did you specify your test suite.Holzer A, Schallhart C, Tautschnig M and Veith H
ASE., 407-416. Editors: Pecheur C, Andrews J and Nitto ED.
01-01-2010
An Introduction to Test Specification in FQL.Holzer A, Tautschnig M, Schallhart C and Veith H
Haifa Verification Conference. vol. 6504, 9-22. Editors: Barner S, Harris IG, Kroening D and Raz O.
01-01-2010
Timely Time Estimates.Holzer A, Januzaj V, Kugele S and Tautschnig M
ISoLA (1). vol. 6415, 33-46. Editors: Margaria T and Steffen B.
01-01-2010
Don't care in SMT: building flexible yet efficient abstraction/refinement solvers.Bauer A, Leucker M, Schallhart C and Tautschnig M
Int. J. Softw. Tools Technol. Transf. vol. 12, 23-37.
01-01-2010
2009
Optimizing Automatic Deployment Using Non-functional Requirement AnnotationsKugele S, Haberl W, Tautschnig M and Wechs M
Communications in Computer and Information Science vol. 17, 400-414.
01-12-2009
Navigating the Requirements JungleLanger B and Tautschnig M
Communications in Computer and Information Science vol. 17, 354-368.
01-12-2009
Short Regular Expressions from Finite Automata: Empirical Results.Gruber H, Holzer M and Tautschnig M
CIAA. vol. 5642, 188-197. Editors: Maneth S.
01-01-2009
Query-Driven Program Testing.Holzer A, Schallhart C, Tautschnig M and Veith H
VMCAI. vol. 5403, 151-166. Editors: Jones ND and Müller-Olm M.
01-01-2009
Generating Distributed Code from Cola ModelsHaberl W, Tautschnig M and Baumgarten U
In Trends in Communication Technologies and Engineering Science, Springer Nature 265-279.
01-01-2009
2008
Navigating the Requirements Jungle.Langer B and Tautschnig M
ISoLA. vol. 17, 354-368. Editors: Margaria T and Steffen B.
01-01-2008
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.Holzer A, Schallhart C, Tautschnig M and Veith H
CAV. vol. 5123, 209-213. Editors: Gupta A and Malik S.
01-01-2008
Optimizing Automatic Deployment Using Non-functional Requirement Annotations.Kugele S, Haberl W, Tautschnig M and Wechs M
ISoLA. vol. 17, 400-414. Editors: Margaria T and Steffen B.
01-01-2008
Automatic generation of systemc models from component-based designs for early design validation and performance analysis.Wang Z, Haberl W, Kugele S and Tautschnig M
WOSP., 139-144. Editors: Avritzer A, Weyuker EJ and Woodside CM.
01-01-2008
A Model Driven Development Approach for Implementing Reactive Systems in Hardware.Wang Z, Herkersdorf A, Merenda S and Tautschnig M
FDL., 197-202.
01-01-2008
A Benchmarking Suite for Measurement-Based WCET Analysis Tools.Bünte S and Tautschnig M
ICST Workshops., 353-356.
01-01-2008
Running COLA on embedded systemsHaberl W, Tautschnig M and Baumgarten U
IMECS 2008: INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II., 922-928.
01-01-2008
A Model Driven Development Approach for Implementing Reactive Systems in HardwareWang Z, Herkersdorf A, Merenda S and Tautschnig M
2008 FORUM ON SPECIFICATION, VERIFICATION AND DESIGN LANGUAGES., 221-+.
01-01-2008
2007
Tool-support for the analysis of hybrid systems and models.Bauer A, Pister M and Tautschnig M
DATE., 924-929. Editors: Lauwereins R and Madsen J.
01-01-2007
Compatibility and reuse in component-based systems via type and unit inference.Kühnel C, Bauer A and Tautschnig M
EUROMICRO-SEAA., 101-108.
01-01-2007
Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers.Bauer A, Leucker M, Schallhart C and Tautschnig M
ISoLA. vol. RNTI-SM-1, 135-146. Editors: Ameur YA, Boniol F and Wiels V.
01-01-2007