Dr Michael Tautschnig

Michael Tautschnig

Lecturer

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

Research

Software Verification, Concurrency, Decision Procedures

Publications

solid heart iconPublications of specific relevance to the Centre for Fundamental Computer Science

2024

Relevant PublicationNeural Model Checking.
Giacobbe M, Kroening D, Pal A and Tautschnig M
 
01-01-2024

2022

bullet iconVerification Witnesses
Beyer 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
Relevant PublicationVerification 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

bullet iconCode-level model checking in the software development workflow at Amazon Web Services
Chong 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

bullet iconUsing model checking tools to triage the severity of security bugs in the Xen hypervisor
Cook B, Döbel B, Kroening D, Manthey N, Pohlack M, Polgreen E, Tautschnig M and Wieczorkiewicz P
Formal Methods in Computer Aided Design
24-09-2020
bullet iconCode-level model checking in the software development workflow
Chong 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
27-06-2020

2019

bullet iconTests from Witnesses Execution-Based Validation of Verification Results
Beyer D, Dangl M, Lemberger T and Tautschnig M
Tests and Proofs
05-07-2019
bullet iconCBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution)
Khazem K and Tautschnig M
 
01-01-2019
bullet iconCBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker
Khazem K and Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 199-203.  
01-01-2019

2018

bullet iconModel Checking Boot Code from AWS Data Centers
Cook B, Khazem K, Kroening D, Tasiran S, TAUTSCHNIG M and Tuttle M
Computer Aided Verification
18-07-2018
bullet iconEffective verification for low-level software with competing interrupts
Liang 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
bullet iconTests from Witnesses
Beyer D, Dangl M, Lemberger T and Tautschnig M
In Tests and Proofs, Springer Nature 3-23.  
01-01-2018

2017

bullet iconVerifyThis 2015 A program verification competition
Huisman M, Klebanov V, Monahan R and Tautschnig M
International Journal On Software Tools For Technology Transfer vol. 19 (6), 763-771.  
19-10-2017
bullet iconConcurrent Program Verification with Invariant-Guided Underapproximation
Prabhu S, Schrammel P, Srivas M, Tautschnig M and Yeolekar A
Automated Technology for Verification and Analysis
27-09-2017

2016

Relevant PublicationInformation leakage analysis of complex C code and its application to OpenSSL
MALACARIA P, TAUTCHNING M and DISTEFANO D
7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016
05-10-2016
bullet iconAssisted Coverage Closure
Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M
Nasa Formal Methods vol. 9690, 49-64.  
04-06-2016
bullet iconv2c – A Verilog to C Translator
Mukherjee R, Tautschnig M and Kroening D
 
01-01-2016
bullet iconsmid: A Black-Box Program Driver
Khazem K and Tautschnig M
 
01-01-2016
bullet iconv2c - A Verilog to C Translator
Mukherjee R, Tautschnig M and Kroening D
Tools and Algorithms for the Construction and Analysis of Systems
01-01-2016
bullet iconAssisted Coverage Closure.
Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P and Tautschnig M
, Editors: Rayadurgam S and Tkachuk O. 
01-01-2016

2015

bullet iconClosure properties and complexity of rational sets of regular languages
Holzer A, Schallhart C, Tautschnig M and Veith H
Theoretical Computer Science, Elsevier vol. 605, 62-79.  
01-11-2015
bullet iconEffective verification of low-level software with nested interrupts
Kroening D, Liang L, Melham T, Schrammel P and Tautschnig M
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015
22-04-2015
bullet iconLearning the Language of Error
Chapman M, Chockler H, Kesseli P, Kroening D, Strichman O and Tautschnig M
 
01-01-2015
bullet iconCBMC: Bounded model checking of concurrent C programs
Tautschnig M
 
01-01-2015

2014

bullet iconAutomating test-suite augmentation
Bloem R, Konighofer R, Rock F and Tautschnig M
2014 14th International Conference on Quality Software
01-10-2014
bullet iconHerding 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
bullet iconHerding cats
Alglave J, Maranget L and Tautschnig M
 
05-06-2014
bullet iconAutomating Software Analysis at Large Scale
Kroening D and Tautschnig M
 
01-01-2014
bullet iconCBMC - C Bounded Model Checker (Competition contribution)
Kroening D and Tautschnig M
 
01-01-2014
bullet iconReusing information in multi-goal reachability analyses
Beyer D, Holzer A, Tautschnig M and Veith H
 
01-01-2014
bullet iconHerding cats: Modelling, simulation, testing, and data-mining for weak memory
Alglave J, Maranget L, Tautschnig M and ACM
 
01-01-2014
bullet iconCBMC – C Bounded Model Checker
Kroening D and Tautschnig M
In Tools and Algorithms For The Construction and Analysis of Systems, Springer Nature 389-391.  
01-01-2014

2013

bullet iconFormal co-validation of low-level hardware/software interfaces
Horn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J and Kroening D
2013 Formal Methods in Computer-Aided Design
06-12-2013
bullet iconHerding Cats - Modelling, simulation, testing, and data-mining for weak memory
Alglave J, Maranget L and Tautschnig M
 
30-08-2013
bullet iconOn the Structure and Complexity of Rational Sets of Regular Languages
Holzer A, Schallhart C, Tautschnig M and Veith H
 
26-05-2013
bullet iconPartial Orders for Efficient BMC of Concurrent Software
Alglave J, Kroening D and Tautschnig M
 
08-01-2013
bullet iconInformation Reuse for Multi-goal Reachability Analyses.
Beyer D, Holzer A, Tautschnig M and Veith H
, Editors: Felleisen M and Gardner P. 
01-01-2013
bullet iconSoftware Verification for Weak Memory via Program Transformation.
Alglave J, Kroening D, Nimal V and Tautschnig M
, Editors: Felleisen M and Gardner P. 
01-01-2013
bullet iconPINCETTE - 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
, Editors: Cleve A, Ricca F and Cerioli M. 
01-01-2013
bullet iconPartial Orders for Efficient Bounded Model Checking of Concurrent Software.
Alglave J, Kroening D and Tautschnig M
, Editors: Sharygina N and Veith H. 
01-01-2013
bullet iconHerding Cats.
Alglave J, Maranget L and Tautschnig M
Corr vol. abs/1308.6810 
01-01-2013
bullet iconOn the Structure and Complexity of Rational Sets of Regular Languages.
Holzer A, Schallhart C, Tautschnig M and Veith H
, Editors: Seth A and Vishnoi NK. 
01-01-2013

2012

bullet iconSoftware Verification for Weak Memory via Program Transformation
Alglave J, Kroening D, Nimal V and Tautschnig M
 
30-07-2012
bullet iconNumeric Bounds Analysis with Conflict-Driven Learning.
D'Silva VV, Haller L, Kroening D and Tautschnig M
, Editors: Flanagan C and König B. 
01-01-2012
bullet iconCounterexample-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
bullet iconProving Reachability Using FShell - (Competition Contribution).
Holzer A, Kroening D, Schallhart C, Tautschnig M and Veith H
, Editors: Flanagan C and König B. 
01-01-2012
bullet iconsatabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).
Basler G, Donaldson AF, Kaiser A, Kroening D, Tautschnig M and Wahl T
, Editors: Flanagan C and König B. 
01-01-2012
bullet iconProving Reachability Using FShell
Holzer 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
bullet iconsatabs: A Bit-Precise Verifier for C Programs
Basler 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

bullet iconSeamless Testing for Models and Code.
Holzer A, Januzaj V, Kugele S, Langer B, Schallhart C, Tautschnig M and Veith H
, Editors: Giannakopoulou D and Orejas F. 
01-01-2011
bullet iconImproving the Confidence in Measurement-Based Timing Analysis.
Bünte S, Zolda M, Tautschnig M and Kirner R
 
01-01-2011
bullet iconSoundness of Data Flow Analyses for Weak Memory Models.
Alglave J, Kroening D, Lugton J, Nimal V and Tautschnig M
, Editors: Yang H. 
01-01-2011
bullet iconMaking Software Verification Tools Really Work.
Alglave J, Donaldson AF, Kroening D and Tautschnig M
, Editors: Bultan T and Hsiung P-A. 
01-01-2011

2010

bullet iconSeamless Model-Driven Development Put into Practice.
Haberl W, Herrmannsdoerfer M, Kugele S, Tautschnig M and Wechs M
, Editors: Margaria T and Steffen B. 
01-01-2010
bullet iconHow did you specify your test suite.
Holzer A, Schallhart C, Tautschnig M and Veith H
, Editors: Pecheur C, Andrews J and Nitto ED. 
01-01-2010
bullet iconAn Introduction to Test Specification in FQL.
Holzer A, Tautschnig M, Schallhart C and Veith H
, Editors: Barner S, Harris IG, Kroening D and Raz O. 
01-01-2010
bullet iconTimely Time Estimates.
Holzer A, Januzaj V, Kugele S and Tautschnig M
, Editors: Margaria T and Steffen B. 
01-01-2010
bullet iconDon'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

bullet iconOptimizing Automatic Deployment Using Non-functional Requirement Annotations
Kugele S, Haberl W, Tautschnig M and Wechs M
Communications in Computer and Information Science vol. 17, 400-414.  
01-12-2009
bullet iconNavigating the Requirements Jungle
Langer B and Tautschnig M
Communications in Computer and Information Science vol. 17, 354-368.  
01-12-2009
bullet iconShort Regular Expressions from Finite Automata: Empirical Results.
Gruber H, Holzer M and Tautschnig M
, Editors: Maneth S. 
01-01-2009
bullet iconQuery-Driven Program Testing.
Holzer A, Schallhart C, Tautschnig M and Veith H
, Editors: Jones ND and Müller-Olm M. 
01-01-2009
bullet iconGenerating Distributed Code from Cola Models
Haberl W, Tautschnig M and Baumgarten U
In Trends in Communication Technologies and Engineering Science, Springer Nature 265-279.  
01-01-2009

2008

bullet iconNavigating the Requirements Jungle.
Langer B and Tautschnig M
, Editors: Margaria T and Steffen B. 
01-01-2008
bullet iconFShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.
Holzer A, Schallhart C, Tautschnig M and Veith H
, Editors: Gupta A and Malik S. 
01-01-2008
bullet iconOptimizing Automatic Deployment Using Non-functional Requirement Annotations.
Kugele S, Haberl W, Tautschnig M and Wechs M
, Editors: Margaria T and Steffen B. 
01-01-2008
bullet iconAutomatic generation of systemc models from component-based designs for early design validation and performance analysis.
Wang Z, Haberl W, Kugele S and Tautschnig M
, Editors: Avritzer A, Weyuker EJ and Woodside CM. 
01-01-2008
bullet iconA Model Driven Development Approach for Implementing Reactive Systems in Hardware.
Wang Z, Herkersdorf A, Merenda S and Tautschnig M
 
01-01-2008
bullet iconA Benchmarking Suite for Measurement-Based WCET Analysis Tools.
Bünte S and Tautschnig M
 
01-01-2008
bullet iconRunning COLA on embedded systems
Haberl W, Tautschnig M and Baumgarten U
 
01-01-2008
bullet iconA Model Driven Development Approach for Implementing Reactive Systems in Hardware
Wang Z, Herkersdorf A, Merenda S and Tautschnig M
 
01-01-2008

2007

bullet iconTool-support for the analysis of hybrid systems and models.
Bauer A, Pister M and Tautschnig M
, Editors: Lauwereins R and Madsen J. 
01-01-2007
bullet iconCompatibility and reuse in component-based systems via type and unit inference.
Kühnel C, Bauer A and Tautschnig M
 
01-01-2007
bullet iconDon't care in SMT-Building flexible yet efficient abstraction/refinement solvers.
Bauer A, Leucker M, Schallhart C and Tautschnig M
, Editors: Ameur YA, Boniol F and Wiels V. 
01-01-2007