School of Electronic Engineering and Computer Science
  1. School of Electronic Engineering and Computer Science
  2. People
  3. Profiles

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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Chapman M, Chockler H, Kesseli P et al. (2015). Learning the Language of Error. nameOfConference
  • 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
  • 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
  • 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 et al. (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. nameOfConference
  • Beyer D, Holzer A, Tautschnig M et al. (2014). Reusing Information in Multi-Goal Reachability Analyses.. nameOfConference
  • Horn A, Tautschnig M, Val C et al. (2013). Formal Co-Validation of Low-Level Hardware/Software Interfaces. nameOfConference
  • Alglave J, Maranget L, Tautschnig M (2013). Herding Cats.. nameOfConference
  • Beyer D, Holzer A, Tautschnig M et al. (2013). Information Reuse for Multi-goal Reachability Analyses.. nameOfConference
  • Holzer A, Schallhart C, Tautschnig M et al. (2013). On the Structure and Complexity of Rational Sets of Regular Languages. nameOfConference
  • Holzer A, Schallhart C, Tautschnig M et al. (2013). On the Structure and Complexity of Rational Sets of Regular Languages.. nameOfConference
  • Chockler H, Denaro G, Ling M et al. (2013). PINCETTE - Validating Changes and Upgrades in Networked Software.. nameOfConference
  • Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient BMC of Concurrent Software. nameOfConference
  • Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient Bounded Model Checking of Concurrent Software.. nameOfConference
  • Alglave J, Kroening D, Nimal V et al. (2013). Software Verification for Weak Memory via Program Transformation. nameOfConference
  • Alglave J, Kroening D, Nimal V et al. (2013). Software Verification for Weak Memory via Program Transformation.. nameOfConference
  • Donaldson AF, Kaiser A, Kroening D et al. (2012). Counterexample-guided abstraction refinement for symmetric concurrent programs.. nameOfConference
  • D'Silva V, Haller L, Kroening D et al. (2012). Numeric Bounds Analysis with Conflict-Driven Learning.. nameOfConference
  • Holzer A, Kroening D, Schallhart C et al. (2012). Proving Reachability Using FShell - (Competition Contribution).. nameOfConference
  • Basler G, Donaldson AF, Kaiser A et al. (2012). satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).. nameOfConference
  • Bünte S, Zolda M, Tautschnig M et al. (2011). Improving the Confidence in Measurement-Based Timing Analysis.. nameOfConference
  • Alglave J, Donaldson AF, Kroening D et al. (2011). Making Software Verification Tools Really Work.. nameOfConference
  • Holzer A, Januzaj V, Kugele S et al. (2011). Seamless Testing for Models and Code.. nameOfConference
  • Alglave J, Kroening D, Lugton J et al. (2011). Soundness of Data Flow Analyses for Weak Memory Models.. nameOfConference
  • Holzer A, Tautschnig M, Schallhart C et al. (2010). An Introduction to Test Specification in FQL.. nameOfConference
  • Bauer A, Leucker M, Schallhart C et al. (2010). Don't care in SMT: building flexible yet efficient abstraction/refinement solvers.. nameOfConference
  • Holzer A, Schallhart C, Tautschnig M et al. (2010). How did you specify your test suite.. nameOfConference
  • Haberl W, Herrmannsdoerfer M, Kugele S et al. (2010). Seamless Model-Driven Development Put into Practice.. nameOfConference
  • Holzer A, Januzaj V, Kugele S et al. (2010). Timely Time Estimates.. nameOfConference
  • Holzer A, Schallhart C, Tautschnig M et al. (2009). Query-Driven Program Testing.. nameOfConference
  • Gruber H, Holzer M, Tautschnig M (2009). Short Regular Expressions from Finite Automata: Empirical Results.. nameOfConference
  • Bünte S, Tautschnig M (2008). A Benchmarking Suite for Measurement-Based WCET Analysis Tools.. nameOfConference
  • Wang Z, Herkersdorf A, Merenda S et al. (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. nameOfConference
  • Wang Z, Herkersdorf A, Merenda S et al. (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware.. nameOfConference
  • 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
  • Holzer A, Schallhart C, Tautschnig M et al. (2008). FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.. nameOfConference
  • Langer B, Tautschnig M (2008). Navigating the Requirements Jungle.. nameOfConference
  • Kugele S, Haberl W, Tautschnig M et al. (2008). Optimizing Automatic Deployment Using Non-functional Requirement Annotations.. nameOfConference
  • Haberl W, Tautschnig M, Baumgarten U et al. (2008). Running COLA on embedded systems. nameOfConference
  • Kühnel C, Bauer A, Tautschnig M (2007). Compatibility and reuse in component-based systems via type and unit inference.. nameOfConference
  • Bauer A, Leucker M, Schallhart C et al. (2007). Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers.. nameOfConference
  • Bauer A, Pister M, Tautschnig M (2007). Tool-support for the analysis of hybrid systems and models.. nameOfConference
  • Khazem K, TAUTSCHNIG M (publicationYear). smid: A Black-Box Program Driver. 23rd International SPIN Symposium on Model Checking of Software