Dr Michael Tautschnig

Research

Research Interests:

Publications

• Khazem K, Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker - (Competition Contribution).. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Cook B, Khazem K, Kroening D et al. (2018). Model Checking Boot Code from AWS Data Centers. Computer Aided Verification

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/44645
• Liang L, Melham T, Kroening D et al. (2018). Effective verification for low-level software with competing interrupts. nameOfConference

  
  

  DOI: 10.1145/3147432

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31940
• Beyer D, Dangl M, Lemberger T et al. (2018). Tests from Witnesses - Execution-Based Validation of Verification Results.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Huisman M, Klebanov V, Monahan R et al. (2017). VerifyThis 2015 A program verification competition. nameOfConference

  
  

  DOI: 10.1007/s10009-016-0438-x

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31939
• Prabhu S, Schrammel P, Srivas MK et al. (2017). Concurrent Program Verification with Invariant-Guided Underapproximation.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Nellis A, Kesseli P, Conmy PR et al. (2016). Assisted Coverage Closure. nameOfConference

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/11330
• Nellis A, Kesseli P, Conmy PR et al. (2016). Assisted Coverage Closure.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Khazem K, Tautschnig M (2016). smid: A Black-Box Program Driver. nameOfConference

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13960
• Mukherjee R, Tautschnig M, Kroening D (2016). v2c - A Verilog to C Translator. Tools and Algorithms for the Construction and Analysis of Systems

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13690
• Mukherjee R, Tautschnig M, Kroening D (2016). v2c-A Verilog to C Translator. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Holzer A, Schallhart C, Tautschnig M et al. (2015). Closure properties and complexity of rational sets of regular languages. nameOfConference

  
  

  DOI: 10.1016/j.tcs.2015.08.035

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/11032
• Kroening D, Liang L, Melham T et al. (2015). Effective Verification of Low-Level Software with Nested Interrupts. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Chapman M, Chockler H, Kesseli P et al. (2015). Learning the Language of Error. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Alglave J, Maranget L, Tautschnig M (2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. nameOfConference

  
  

  DOI: 10.1145/2627752

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/11250
• Alglave J, Maranget L, Tautschnig M (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. nameOfConference

  
  

  DOI: 10.1145/2666356.2594347

  
  

  QMRO: qmroHref
• Kroening D, Tautschnig M (2014). Automating Software Analysis at Large Scale. nameOfConference

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/12009
• Bloem R, Koenighofer R, Roeck F et al. (2014). Automating Test-Suite Augmentation. nameOfConference

  
  

  DOI: 10.1109/QSIC.2014.40

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/11249
• Kroening D, Tautschnig M (2014). CBMC - C Bounded Model Checker - (Competition Contribution).. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Maranget L, Tautschnig M (2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Maranget L, Tautschnig M et al. (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. nameOfConference

  
  

  DOI: 10.1145/2594291.2594347

  
  

  QMRO: qmroHref
• Beyer D, Holzer A, Tautschnig M et al. (2014). Reusing Information in Multi-Goal Reachability Analyses.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Horn A, Tautschnig M, Val C et al. (2013). Formal Co-Validation of Low-Level Hardware/Software Interfaces. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Maranget L, Tautschnig M (2013). Herding Cats.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Beyer D, Holzer A, Tautschnig M et al. (2013). Information Reuse for Multi-goal Reachability Analyses.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Holzer A, Schallhart C, Tautschnig M et al. (2013). On the Structure and Complexity of Rational Sets of Regular Languages. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/12016
• Holzer A, Schallhart C, Tautschnig M et al. (2013). On the Structure and Complexity of Rational Sets of Regular Languages.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Chockler H, Denaro G, Ling M et al. (2013). PINCETTE - Validating Changes and Upgrades in Networked Software.. nameOfConference

  
  

  DOI: 10.1109/CSMR.2013.72

  
  

  QMRO: qmroHref
• Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient BMC of Concurrent Software. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/3659
• Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient Bounded Model Checking of Concurrent Software.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Kroening D, Nimal V et al. (2013). Software Verification for Weak Memory via Program Transformation. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/3679
• Alglave J, Kroening D, Nimal V et al. (2013). Software Verification for Weak Memory via Program Transformation.. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Donaldson AF, Kaiser A, Kroening D et al. (2012). Counterexample-guided abstraction refinement for symmetric concurrent programs.. nameOfConference

  
  

  DOI: 10.1007/s10703-012-0155-3

  
  

  QMRO: qmroHref
• D'Silva V, Haller L, Kroening D et al. (2012). Numeric Bounds Analysis with Conflict-Driven Learning.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Holzer A, Kroening D, Schallhart C et al. (2012). Proving Reachability Using FShell - (Competition Contribution).. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Basler G, Donaldson AF, Kaiser A et al. (2012). satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Bünte S, Zolda M, Tautschnig M et al. (2011). Improving the Confidence in Measurement-Based Timing Analysis.. nameOfConference

  
  

  DOI: 10.1109/ISORC.2011.27

  
  

  QMRO: qmroHref
• Alglave J, Donaldson AF, Kroening D et al. (2011). Making Software Verification Tools Really Work.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Holzer A, Januzaj V, Kugele S et al. (2011). Seamless Testing for Models and Code.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Kroening D, Lugton J et al. (2011). Soundness of Data Flow Analyses for Weak Memory Models.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Holzer A, Tautschnig M, Schallhart C et al. (2010). An Introduction to Test Specification in FQL.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Bauer A, Leucker M, Schallhart C et al. (2010). Don't care in SMT: building flexible yet efficient abstraction/refinement solvers.. nameOfConference

  
  

  DOI: 10.1007/s10009-009-0133-2

  
  

  QMRO: qmroHref
• Holzer A, Schallhart C, Tautschnig M et al. (2010). How did you specify your test suite.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Haberl W, Herrmannsdoerfer M, Kugele S et al. (2010). Seamless Model-Driven Development Put into Practice.. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Holzer A, Januzaj V, Kugele S et al. (2010). Timely Time Estimates.. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Holzer A, Schallhart C, Tautschnig M et al. (2009). Query-Driven Program Testing.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Gruber H, Holzer M, Tautschnig M (2009). Short Regular Expressions from Finite Automata: Empirical Results.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Bünte S, Tautschnig M (2008). A Benchmarking Suite for Measurement-Based WCET Analysis Tools.. nameOfConference

  
  

  DOI: 10.1109/ICSTW.2008.1

  
  

  QMRO: qmroHref
• Wang Z, Herkersdorf A, Merenda S et al. (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Wang Z, Herkersdorf A, Merenda S et al. (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• 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

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Holzer A, Schallhart C, Tautschnig M et al. (2008). FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Langer B, Tautschnig M (2008). Navigating the Requirements Jungle.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Kugele S, Haberl W, Tautschnig M et al. (2008). Optimizing Automatic Deployment Using Non-functional Requirement Annotations.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Haberl W, Tautschnig M, Baumgarten U et al. (2008). Running COLA on embedded systems. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Kühnel C, Bauer A, Tautschnig M (2007). Compatibility and reuse in component-based systems via type and unit inference.. nameOfConference

  
  

  DOI: 10.1109/EUROMICRO.2007.24

  
  

  QMRO: qmroHref
• Bauer A, Leucker M, Schallhart C et al. (2007). Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Bauer A, Pister M, Tautschnig M (2007). Tool-support for the analysis of hybrid systems and models.. nameOfConference

  
  

  DOI: 10.1109/DATE.2007.364411

  
  

  QMRO: qmroHref