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

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

    DOI: doi


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



    Citations: 0
  • Beyer D, Dangl M, Lemberger T et al. (2018). Tests from Witnesses - Execution-Based Validation of Verification Results.. nameOfConference

    DOI: doi

    QMRO: qmroHref

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



    Citations: 0
  • Prabhu S, Schrammel P, Srivas MK et al. (2017). Concurrent Program Verification with Invariant-Guided Underapproximation.. nameOfConference

    DOI: doi

    QMRO: qmroHref

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



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

    DOI: doi

    QMRO: qmroHref

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



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



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


    QMRO: qmroHref

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



    Citations: 1
  • Kroening D, Liang L, Melham T et al. (2015). Effective Verification of Low-Level Software with Nested Interrupts. nameOfConference

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

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



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


    QMRO: qmroHref

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



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



    Citations: 2
  • Kroening D, Tautschnig M (2014). CBMC - C Bounded Model Checker - (Competition Contribution).. nameOfConference

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi


    Citations: 0
  • 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

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


    QMRO: qmroHref

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

    DOI: doi


    Citations: 0
  • Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient Bounded Model Checking of Concurrent Software.. nameOfConference

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi


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


    QMRO: qmroHref

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


    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

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


    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

    Citations: 0
  • 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

    Citations: 0
  • 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

    Citations: 0
  • 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

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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

    DOI: doi

    QMRO: qmroHref

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


    QMRO: qmroHref

    Citations: 0
  • 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

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


    QMRO: qmroHref

    Citations: 0
  • Khazem K, TAUTSCHNIG M (publicationYear). smid: A Black-Box Program Driver. 23rd International SPIN Symposium on Model Checking of Software



    Citations: 0