Dr Michael Tautschnig

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:

Publications

• 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

  
  

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

  
  

  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

  
  

  DOI: 10.1007/s10009-016-0438-x

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31939

  
  

  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

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/11330

  
  

  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

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13960

  
  

  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

  
  

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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13690

  
  

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

  
  

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

  
  

  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

  
  

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

  
  

  QMRO: qmroHref

  
  

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

  
  

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

  
  

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

  
  

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

  
  

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

  
  

  DOI: 10.1145/2594291.2594347

  
  

  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: 10
• 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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/12016

  
  

  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

  
  

  DOI: 10.1109/CSMR.2013.72

  
  

  QMRO: qmroHref

  
  

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

  
  

  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

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/3679

  
  

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

  
  

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

  
  

  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

  
  

  DOI: 10.1109/ISORC.2011.27

  
  

  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

  
  

  DOI: 10.1007/s10009-009-0133-2

  
  

  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

  
  

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

  
  

  QMRO: qmroHref

  
  

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

  
  

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

  
  

  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

  
  

  DOI: 10.1109/ICSTW.2008.1

  
  

  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

  
  

  DOI: 10.1109/EUROMICRO.2007.24

  
  

  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

  
  

  DOI: 10.1109/DATE.2007.364411

  
  

  QMRO: qmroHref

  
  

  Citations: 0