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

Teaching

Microprocessor Systems Design (Undergraduate)

This module examines the structure, applications and programming of microcontroller and similar devices. There will be practical work on using the devices as part of the module. Aims: * To impart an understanding of the architectures of microcontrollers microprocessors, and PIC devices. * To impart an understanding of the design issues in using microcontrollers and similar devices. * To enable students to make an informed choice of microcontrollers or similar device for a particular application. * To enable students to use microcontroller devices in electronic circuits.

Software Analysis and Verification (Undergraduate)

Software analysis and verification is about being able to rigorously analyse and verify software. While testing is a very effective way to eliminate software bugs, it cannot guarantee their elimination. Tools based on logics as introduced in ECS715P 'Programme Specifications' are more and more effective in providing strong guarantees in the analysis and verification of software, in particular in the elimination of software bugs.

Software Analysis and Verification (Postgraduate)

The module will cover: 1. Introduction to Logic for Systems and Program Verification and Analysis 2. Using Hoare Logic: The specification language - describing properties of programs; Proof rules in Hoare logic - verifying properties of programs; Basic technologies behind building automatic program verification tools based on Hoare logic; Using automatic verification tools based on Hoare logic. 3. Introduction to modelchecking and Spin: Temporal logic: modelling states and operations of a system; Modelchecking logics in particular CTL; Safety and Liveness in systems; Using Spin for checking properties and for problem solving.

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