Dr Michael Tautschnig
Lecturer
Email: michael.tautschnig@qmul.ac.ukTelephone: +44 20 7882 5226Room Number: Peter Landin, CS 432Website: http://www.tautschnig.netOffice 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 VerificationConcurrency
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
DOI: 10.1145/3147432
-
Huisman M, Klebanov V, Monahan R et al. (2017). VerifyThis 2015 A program verification competition. 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
QMRO: qmroHref -
Holzer A, Schallhart C, Tautschnig M et al. (2015). Closure properties and complexity of rational sets of regular languages. nameOfConference
-
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
DOI: 10.1145/2627752
-
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
DOI: 10.1109/QSIC.2014.40
-
Alglave J, Maranget L, Tautschnig M et al. (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. nameOfConference
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
-
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 -
Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient BMC of Concurrent Software. nameOfConference
DOI: doi
-
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 -
Bünte S, Zolda M, Tautschnig M et al. (2011). Improving the Confidence in Measurement-Based Timing Analysis.. nameOfConference
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 -
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 -
Bünte S, Tautschnig M (2008). A Benchmarking Suite for Measurement-Based WCET Analysis Tools.. nameOfConference
DOI: 10.1109/ICSTW.2008.1
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, Pister M, Tautschnig M (2007). Tool-support for the analysis of hybrid systems and models.. nameOfConference
QMRO: qmroHref