Dr Michael Tautschnig

Lecturer

School of Electronic Engineering and Computer Science
Queen Mary University of London

michael.tautschnig@qmul.ac.uk

www.qmul.ac.uk/eecs/people/profiles/tautschnigmichael.html

Centre for Fundamentals of AI and Computational Theory

Research
Publications
Research Group
News

Research

Software Verification, Concurrency, Decision Procedures

Publications

2024

Neural Model Checking
Giacobbe M Kroening D Pal A Tautschnig M
In Arxiv

DOI 10.48550/arxiv.2410.23790

QMRO

31-10-2024

Neural Model Checking.
Giacobbe M Kroening D Tautschnig M Globersons A Mackey L Belgrave D Fan A Paquet U et al.
NeurIPS.

QMRO

01-01-2024

2023

CBMC: The C Bounded Model Checker
Kroening D Schrammel P Tautschnig M
In Arxiv

DOI 10.48550/arxiv.2302.02384

QMRO

05-02-2023

2022

Verification Witnesses
Beyer D Dangl M Heizmann M Lemberger T
Acm Transactions on Software Engineering and Methodology, Association For Computing Machinery (Acm) vol. 31 (4)

DOI 10.1145/3477579

QMRO

08-09-2022

Verification Witnesses.
Beyer D Dangl M Dietsch D Heizmann M
Acm Trans. Softw. Eng. Methodol. vol. 31, 57:1-57:1.

QMRO

01-01-2022

2021

Code-level model checking in the software development workflow at Amazon Web Services
Chong N Cook B Eidelman J Kallas K Khazem K Monteiro FR Tasiran S Tautschnig M
Software - Practice and Experience vol. 51 (4), 772-797.

DOI 10.1002/spe.2949

QMRO

01-04-2021

2020

Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Cook B Döbel B Kroening D Manthey N Polgreen E
Formal Methods in Computer Aided Design. vol. 00, 185-193.

DOI 10.34727/2020/isbn.978-3-85448-042-6_26

QMRO

24-09-2020

2019

Tests from Witnesses Execution-Based Validation of Verification Results
Beyer D Dangl M Lemberger T
Tests and Proofs. vol. 10889, 3-23.

DOI 10.1007/978-3-319-92994-1_1

QMRO

05-07-2019

CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution)
Khazem K Tautschnig M
Lecture Notes in Computer Science. vol. 11429 LNCS, 199-203.

DOI 10.1007/978-3-030-17502-3_13

01-01-2019

CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker
Khazem K
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 199-203.

DOI 10.1007/978-3-030-17502-3_13

01-01-2019

2018

Model Checking Boot Code from AWS Data Centers
Cook B Khazem K Kroening D TAUTSCHNIG M Tuttle M
Computer Aided Verification.

DOI 10.1007/978-3-319-96142-2_28

QMRO

18-07-2018

Effective verification for low-level software with competing interrupts
Liang L Melham T Kroening D
Acm Transactions on Embedded Computing Systems, Association For Computing Machinery vol. 17, 1-26.

DOI 10.1145/3147432

QMRO

02-01-2018

Tests from Witnesses
Beyer D Dangl M Lemberger T
In Tests and Proofs, Springer Nature 3-23.

DOI 10.1007/978-3-319-92994-1_1

01-01-2018

2017

VerifyThis 2015 A program verification competition
Huisman M Klebanov V
International Journal on Software Tools For Technology Transfer vol. 19 (6), 763-771.

DOI 10.1007/s10009-016-0438-x

QMRO

19-10-2017

Concurrent Program Verification with Invariant-Guided Underapproximation
Prabhu S Srivas M Tautschnig M Yeolekar A
Automated Technology for Verification and Analysis. vol. 10482, 241-248.

DOI 10.1007/978-3-319-68167-2_17

QMRO

27-09-2017

2016

Information leakage analysis of complex C code and its application to OpenSSL
MALACARIA P TAUTCHNING M DISTEFANO D
7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016.

DOI 10.1007/978-3-319-47166-2_63

QMRO

05-10-2016

Assisted Coverage Closure
Nellis A Kesseli P Conmy PR Kroening D
Nasa Formal Methods vol. 9690, 49-64.

DOI 10.1007/978-3-319-40648-0_5

QMRO

04-06-2016

smid: A Black-Box Program Driver
Khazem K 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.

DOI 10.1007/978-3-319-32582-8_12

QMRO

01-01-2016

v2c - A Verilog to C Translator
Mukherjee R Tautschnig M
Tools and Algorithms for the Construction and Analysis of Systems., 580-586.

DOI 10.1007/978-3-662-49674-9_38

QMRO

01-01-2016

Assisted Coverage Closure.
Nellis A Kesseli P Conmy PR Kroening D Rayadurgam S Tkachuk O
NFM. vol. 9690, 49-64.
01-01-2016

smid: A Black-Box Program Driver
Khazem K Tautschnig M
In Model Checking Software, Springer Nature 182-188.

DOI 10.1007/978-3-319-32582-8_12

01-01-2016

2015

Closure properties and complexity of rational sets of regular languages
Holzer A Schallhart C
Theoretical Computer Science, Elsevier vol. 605, 62-79.

DOI 10.1016/j.tcs.2015.08.035

QMRO

01-11-2015

Assisted Coverage Closure
Nellis A Kesseli P Conmy PR Kroening D
In Arxiv

DOI 10.48550/arxiv.1509.04587

15-09-2015

Effective verification of low-level software with nested interrupts
Kroening D Liang L Schrammel P
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015., 229-234.

DOI 10.7873/date.2015.0360

22-04-2015

Learning the Language of Error
Chapman M Chockler H Kesseli P Kroening D
Lecture Notes in Computer Science. vol. 9364, 114-130.

DOI 10.1007/978-3-319-24953-7_9

01-01-2015

CBMC: Bounded model checking of concurrent C programs
Tautschnig 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 augmentation
Bloem R Konighofer R Tautschnig M
2014 14th International Conference on Quality Software., 67-72.

DOI 10.1109/qsic.2014.40

QMRO

01-10-2014

Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.
Alglave J Maranget L
Acm Transactions on Programming Languages and Systems, Association For Computing Machinery vol. 36 (2), 1-74.

DOI 10.1145/2627752

01-07-2014

Herding cats
Alglave J Maranget L Tautschnig M
ACM SIGPLAN Notices. vol. 49 (6), 40-40.

DOI 10.1145/2666356.2594347

05-06-2014

Automating Software Analysis at Large Scale
Kroening D Tautschnig M
Lecture Notes in Computer Science. vol. 8934, 30-39.

DOI 10.1007/978-3-319-14896-0_3

QMRO

01-01-2014

CBMC - C Bounded Model Checker (Competition contribution)
Kroening D Tautschnig M
Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics. vol. 8413 LNCS, 389-391.

DOI 10.1007/978-3-642-54862-8_26

01-01-2014

Reusing information in multi-goal reachability analyses
Beyer D Holzer A Tautschnig M
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 memory
Alglave J Maranget L Tautschnig M
PLDI'14: PROCEEDINGS OF THE 2014 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION., 40-40.

DOI 10.1145/2594291.2594347

01-01-2014

CBMC – C Bounded Model Checker
Kroening D Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 389-391.

DOI 10.1007/978-3-642-54862-8_26

01-01-2014

2013

Formal co-validation of low-level hardware/software interfaces
Horn A Tautschnig M Val C Liang L Melham T
2013 Formal Methods in Computer-Aided Design., 121-128.

DOI 10.1109/fmcad.2013.6679400

06-12-2013

Herding Cats - Modelling, simulation, testing, and data-mining for weak memory
Alglave J Maranget L

DOI 10.1145/2627752

QMRO

30-08-2013

Herding Cats - Modelling, simulation, testing, and data-mining for weak memory
Alglave J Maranget L
In Arxiv

DOI 10.48550/arxiv.1308.6810

30-08-2013

On the Structure and Complexity of Rational Sets of Regular Languages
Holzer A Schallhart C Tautschnig M
In Arxiv

DOI 10.48550/arxiv.1305.6074

26-05-2013

Partial Orders for Efficient BMC of Concurrent Software
Alglave J Kroening D Tautschnig M
In Arxiv

DOI 10.48550/arxiv.1301.1629

08-01-2013

Information Reuse for Multi-goal Reachability Analyses.
Beyer D Holzer A Tautschnig M Felleisen M Gardner P
ESOP. vol. 7792, 472-491.

DOI 10.1007/978-3-642-37036-6_26

01-01-2013

Software Verification for Weak Memory via Program Transformation.
Alglave J Kroening D Nimal V Felleisen M Gardner P
Proceedings of 22nd European Symposium on Programming. vol. 7792, 512-532.

DOI 10.1007/978-3-642-37036-6_28

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 et al.
CSMR., 461-464.

DOI 10.1109/CSMR.2013.72

01-01-2013

Partial Orders for Efficient Bounded Model Checking of Concurrent Software.
Alglave J Kroening D Sharygina N Veith H
CAV. vol. 8044, 141-157.

DOI 10.1007/978-3-642-39799-8_9

01-01-2013

Herding Cats.
Alglave J Maranget L
Corr vol. abs/1308.6810
01-01-2013

On the Structure and Complexity of Rational Sets of Regular Languages.
Holzer A Tautschnig M Seth A Vishnoi NK
FSTTCS. vol. 24, 377-388.
01-01-2013

2012

Software Verification for Weak Memory via Program Transformation
Alglave J Kroening D
In Arxiv

DOI 10.48550/arxiv.1207.7264

30-07-2012

Numeric Bounds Analysis with Conflict-Driven Learning.
D'Silva VV Haller L Kroening D Flanagan C König B
TACAS. vol. 7214, 48-63.

DOI 10.1007/978-3-642-28756-5_5

01-01-2012

Counterexample-guided abstraction refinement for symmetric concurrent programs.
Donaldson AF Kaiser A Kroening D
Formal Methods Syst. Des. vol. 41, 25-44.

DOI 10.1007/s10703-012-0155-3

01-01-2012

Proving Reachability Using FShell - (Competition Contribution).
Holzer A Kroening D Schallhart C Tautschnig M Flanagan C König B
TACAS. vol. 7214, 538-541.

DOI 10.1007/978-3-642-28756-5_43

01-01-2012

satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).
Basler G Donaldson AF Kaiser A Kroening D Tautschnig M Flanagan C König B
TACAS. vol. 7214, 552-555.

DOI 10.1007/978-3-642-28756-5_47

01-01-2012

Proving Reachability Using FShell
Holzer A Schallhart C Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 538-541.

DOI 10.1007/978-3-642-28756-5_43

01-01-2012

satabs: A Bit-Precise Verifier for C Programs
Basler G Donaldson A Kaiser A Kroening D Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 552-555.

DOI 10.1007/978-3-642-28756-5_47

01-01-2012

2011

Seamless Testing for Models and Code.
Holzer A Januzaj V Kugele S Langer B Schallhart C Giannakopoulou D Orejas F
FASE. vol. 6603, 278-293.

DOI 10.1007/978-3-642-19811-3_20

01-01-2011

Improving the Confidence in Measurement-Based Timing Analysis.
Bünte S Tautschnig M
ISORC., 144-151.

DOI 10.1109/ISORC.2011.27

01-01-2011

Soundness of Data Flow Analyses for Weak Memory Models.
Alglave J Kroening D Lugton J Nimal V Yang H
APLAS. vol. 7078, 272-288.

DOI 10.1007/978-3-642-25318-8_21

01-01-2011

Making Software Verification Tools Really Work.
Alglave J Donaldson AF Kroening D Bultan T Hsiung P-A
ATVA. vol. 6996, 28-42.

DOI 10.1007/978-3-642-24372-1_3

01-01-2011

2010

Seamless Model-Driven Development Put into Practice.
Haberl W Herrmannsdoerfer M Tautschnig M Margaria T Steffen B
ISoLA (1). vol. 6415, 18-32.

DOI 10.1007/978-3-642-16558-0_4

01-01-2010

How did you specify your test suite.
Holzer A Schallhart C Veith H Pecheur C Andrews J Nitto ED
ASE., 407-416.

DOI 10.1145/1858996.1859084

01-01-2010

An Introduction to Test Specification in FQL.
Holzer A Tautschnig M Schallhart C Barner S Harris IG Kroening D Raz O
Haifa Verification Conference. vol. 6504, 9-22.

DOI 10.1007/978-3-642-19583-9_5

01-01-2010

Timely Time Estimates.
Holzer A Januzaj V Kugele S Margaria T Steffen B
ISoLA (1). vol. 6415, 33-46.

DOI 10.1007/978-3-642-16558-0_5

01-01-2010

Don't care in SMT: building flexible yet efficient abstraction/refinement solvers.
Bauer A Leucker M Schallhart C
Int. J. Softw. Tools Technol. Transf. vol. 12, 23-37.

DOI 10.1007/s10009-009-0133-2

01-01-2010

2009

Optimizing Automatic Deployment Using Non-functional Requirement Annotations
Kugele S Tautschnig M Wechs M
Communications in Computer and Information Science vol. 17, 400-414.
01-12-2009

Navigating the Requirements Jungle
Langer B 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 Maneth S
CIAA. vol. 5642, 188-197.

DOI 10.1007/978-3-642-02979-0_22

01-01-2009

Query-Driven Program Testing.
Holzer A Schallhart C Tautschnig M Jones ND Müller-Olm M
VMCAI. vol. 5403, 151-166.

DOI 10.1007/978-3-540-93900-9_15

01-01-2009

Generating Distributed Code from Cola Models
Haberl W Baumgarten U
In Trends in Communication Technologies and Engineering Science, Springer Nature 265-279.

DOI 10.1007/978-1-4020-9532-0_20

01-01-2009

2008

Navigating the Requirements Jungle.
Langer B Tautschnig M Margaria T Steffen B
ISoLA. vol. 17, 354-368.

DOI 10.1007/978-3-540-88479-8_25

01-01-2008

FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.
Holzer A Schallhart C Tautschnig M Gupta A Malik S
CAV. vol. 5123, 209-213.

DOI 10.1007/978-3-540-70545-1_20

01-01-2008

Optimizing Automatic Deployment Using Non-functional Requirement Annotations.
Kugele S Haberl W Tautschnig M Margaria T Steffen B
ISoLA. vol. 17, 400-414.

DOI 10.1007/978-3-540-88479-8_28

01-01-2008

Automatic generation of systemc models from component-based designs for early design validation and performance analysis.
Wang Z Haberl W Tautschnig M Avritzer A Weyuker EJ Woodside CM
WOSP., 139-144.

DOI 10.1145/1383559.1383577

01-01-2008

A Model Driven Development Approach for Implementing Reactive Systems in Hardware.
Wang Z Merenda S Tautschnig M
FDL., 197-202.

DOI 10.1109/FDL.2008.4641445

01-01-2008

A Benchmarking Suite for Measurement-Based WCET Analysis Tools.
Bünte S
ICST Workshops., 353-356.

DOI 10.1109/ICSTW.2008.1

01-01-2008

Running COLA on embedded systems
Haberl W Tautschnig M
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 Hardware
Wang Z Herkersdorf A 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 Tautschnig M Lauwereins R Madsen J
DATE., 924-929.

DOI 10.1109/DATE.2007.364411

01-01-2007

Compatibility and reuse in component-based systems via type and unit inference.
Kühnel C Bauer A Tautschnig M
EUROMICRO-SEAA., 101-108.

DOI 10.1109/EUROMICRO.2007.24

01-01-2007

Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers.
Bauer A Leucker M Tautschnig M Ameur YA Boniol F Wiels V
ISoLA. vol. RNTI-SM-1, 135-146.
01-01-2007

Neural Model Checking
Giacobbe M Kroening D Pal A Tautschnig M
Neural Information Processing Systems.

QMRO

Home Page
Tautschnig M

smid: A Black-Box Program Driver
TAUTSCHNIG M Khazem KK
23rd International SPIN Symposium on Model Checking of Software.

DOI 10.1007/978-3-662-49674-9_38

Code Level Model-Checking in the Software Development Workflow
Chong N Cook B KHAZEM K Kallas K Monteiro F Schwartz-Narbonne D Tasiran S Tautschnig M et al.
International Conference on Software Engineering.

DOI 10.1145/3377813.3381347

QMRO

Dr Michael Tautschnig

Research

Publications

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

Research Group

News