Dr Michael Tautschnig

Teaching

Programming for Artificial Intelligence and Data Science (Postgraduate)

This module provides an intensive practical introduction to programming in Python, suitable for students with some degree of mathematical or statistical maturity. It covers a range of practical skills and underlying knowledge. These include the basic programming constructs for control, data structuring and modularisation; the use of systems for collaborative development and version control such as Git; unit testing and documentation; project structures and continuous integration/deployment.

Research

Research Interests:

Publications

• Beyer D, Dangl M, Dietsch D et al. (2022). Verification Witnesses. nameOfConference

  
  

  DOI: 10.1145/3477579

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/92291
• Chong N, Cook B, Eidelman J et al. (2021). Code-level model checking in the software development workflow at Amazon Web Services. nameOfConference

  
  

  DOI: 10.1002/spe.2949

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/70863
• Cook B, Döbel B, Kroening D et al. (2020). Using model checking tools to triage the severity of security bugs in the Xen hypervisor. Formal Methods in Computer Aided Design

  
  

  DOI: 10.34727/2020/isbn.978-3-85448-042-6_26

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/70263
• Chong N, Cook B, Kallas K et al. (2020). Code-level model checking in the software development workflow. nameOfConference

  
  

  DOI: 10.1145/3377813.3381347

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/63239
• Beyer D, Dangl M, Lemberger T et al. (2019). Tests from Witnesses Execution-Based Validation of Verification Results. Tests and Proofs

  
  

  DOI: 10.1007/978-3-319-92994-1_1

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/70261
• Khazem K, Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker. nameOfConference

  
  

  DOI: 10.1007/978-3-030-17502-3_13

  
  

  QMRO: qmroHref
• Khazem K, Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution). nameOfConference

  
  

  DOI: 10.1007/978-3-030-17502-3_13

  
  

  QMRO: qmroHref
• 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
• Beyer D, Dangl M, Lemberger T et al. (2018). Tests from Witnesses. nameOfConference

  
  

  DOI: 10.1007/978-3-319-92994-1_1

  
  

  QMRO: qmroHref
• 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
• 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
• Prabhu S, Schrammel P, Srivas M et al. (2017). Concurrent Program Verification with Invariant-Guided Underapproximation. Automated Technology for Verification and Analysis

  
  

  DOI: 10.1007/978-3-319-68167-2_17

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/70262
• MALACARIA P, TAUTCHNING M, DISTEFANO D (2016). Information leakage analysis of complex C code and its application to OpenSSL. 7th International Symposium on Leveraging Applications

  
  

  DOI: 10.1007/978-3-319-47166-2_63

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13880
• 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
• Nellis A, Kesseli P, Conmy PR et al. (2016). Assisted Coverage Closure.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• 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
• 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
• 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
• 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
• Kroening D, Liang L, Melham T et al. (2015). Effective verification of low-level software with nested interrupts. nameOfConference

  
  

  DOI: 10.7873/date.2015.0360

  
  

  QMRO: qmroHref
• Tautschnig M (2015). CBMC: Bounded model checking of concurrent C programs. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• 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
• Bloem R, Koenighofer R, Rock 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
• Alglave J, Maranget L, Tautschnig M (2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.. nameOfConference

  
  

  DOI: 10.1145/2627752

  
  

  QMRO: qmroHref
• 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
• Kroening D, Tautschnig M (2014). CBMC - C Bounded Model Checker (Competition contribution). nameOfConference

  
  

  DOI: 10.1007/978-3-642-54862-8_26

  
  

  QMRO: qmroHref
• Kroening D, Tautschnig M (2014). CBMC – C Bounded Model Checker. nameOfConference

  
  

  DOI: 10.1007/978-3-642-54862-8_26

  
  

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

  
  

  DOI: 10.1145/2594291.2594347

  
  

  QMRO: qmroHref
• Beyer D, Holzer A, Tautschnig M et al. (2014). Reusing information in multi-goal reachability analyses. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Alglave J, Maranget L, Tautschnig M (2013). 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
• Holzer A, Schallhart C, Tautschnig M et al. (2013). On the Structure and Complexity of Rational Sets of Regular Languages. nameOfConference

  
  

  DOI: 10.4230/LIPIcs.FSTTCS.2013.377

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/12016
• 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
• Horn A, Tautschnig M, Val C et al. (2013). Formal co-validation of low-level hardware/software interfaces. nameOfConference

  
  

  DOI: 10.1109/fmcad.2013.6679400

  
  

  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: 10.1007/978-3-642-37036-6_26

  
  

  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

  
  

  QMRO: qmroHref
• 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 Bounded Model Checking of Concurrent Software.. nameOfConference

  
  

  DOI: 10.1007/978-3-642-39799-8_9

  
  

  QMRO: qmroHref
• 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
• Alglave J, Kroening D, Nimal V et al. (2012). Software Verification for Weak Memory via Program Transformation. nameOfConference

  
  

  DOI: 10.1007/978-3-642-37036-6_28

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/3679
• 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
• D'Silva V, Haller L, Kroening D et al. (2012). Numeric Bounds Analysis with Conflict-Driven Learning.. nameOfConference

  
  

  DOI: 10.1007/978-3-642-28756-5_5

  
  

  QMRO: qmroHref
• Holzer A, Kroening D, Schallhart C et al. (2012). Proving Reachability Using FShell. nameOfConference

  
  

  DOI: 10.1007/978-3-642-28756-5_43

  
  

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

  
  

  DOI: 10.1007/978-3-642-28756-5_43

  
  

  QMRO: qmroHref
• Basler G, Donaldson A, Kaiser A et al. (2012). satabs: A Bit-Precise Verifier for C Programs. nameOfConference

  
  

  DOI: 10.1007/978-3-642-28756-5_47

  
  

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

  
  

  DOI: 10.1007/978-3-642-28756-5_47

  
  

  QMRO: qmroHref
• 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
• Alglave J, Donaldson AF, Kroening D et al. (2011). Making Software Verification Tools Really Work.. nameOfConference

  
  

  DOI: 10.1007/978-3-642-24372-1_3

  
  

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

  
  

  DOI: 10.1007/978-3-642-19811-3_20

  
  

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

  
  

  DOI: 10.1007/978-3-642-25318-8_21

  
  

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

  
  

  DOI: 10.1007/978-3-642-19583-9_5

  
  

  QMRO: qmroHref
• 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
• Holzer A, Schallhart C, Tautschnig M et al. (2010). How did you specify your test suite.. nameOfConference

  
  

  DOI: 10.1145/1858996.1859084

  
  

  QMRO: qmroHref
• 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
• Holzer A, Januzaj V, Kugele S et al. (2010). Timely Time Estimates.. nameOfConference

  
  

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

  
  

  QMRO: qmroHref
• Langer B, Tautschnig M (2009). Navigating the Requirements Jungle. nameOfConference

  
  

  DOI: doi

  
  

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

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Haberl W, Tautschnig M, Baumgarten U (2009). Generating distributed code from cola models. nameOfConference

  
  

  DOI: 10.1007/978-1-4020-9532-0_20

  
  

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

  
  

  DOI: 10.1007/978-3-540-93900-9_15

  
  

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

  
  

  DOI: 10.1007/978-3-642-02979-0_22

  
  

  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
• 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: 10.1109/FDL.2008.4641445

  
  

  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: 10.1145/1383559.1383577

  
  

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

  
  

  DOI: 10.1007/978-3-540-70545-1_20

  
  

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

  
  

  DOI: 10.1007/978-3-540-88479-8_25

  
  

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

  
  

  DOI: 10.1007/978-3-540-88479-8_28

  
  

  QMRO: qmroHref
• Haberl W, Tautschnig M, Baumgarten U (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

  
  

  DOI: 10.1109/EUROMICRO.2007.24

  
  

  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

  
  

  DOI: 10.1109/DATE.2007.364411

  
  

  QMRO: qmroHref