Skip to main content
School of Electronic Engineering and Computer Science

Dr Michael Tautschnig

Michael

Lecturer

Email: michael.tautschnig@qmul.ac.uk
Telephone: +44 20 7882 5226
Room Number: Peter Landin, CS 432
Website: http://www.tautschnig.net
Office Hours: Tuesday 13:00-14:30

Research

Research Interests:

Software Verification
Concurrency
Decision Procedures

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


  • Liang L, Melham T, Kroening D et al. (2018). Effective verification for low-level software with competing interrupts. nameOfConference


  • 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


  • 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


  • 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


  • Mukherjee R, Tautschnig M, Kroening D (2016). v2c - A Verilog to C Translator. Tools and Algorithms for the Construction and Analysis of Systems


  • Mukherjee R, Tautschnig M, Kroening D (2016). v2c-A Verilog to C Translator. nameOfConference


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


  • 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


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


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


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


  • Bloem R, Koenighofer R, Roeck F et al. (2014). Automating Test-Suite Augmentation. nameOfConference


  • 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


    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

  • 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


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

    DOI: doi

  • 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

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


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


    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


    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


    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


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


    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


    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


    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


    QMRO: qmroHref