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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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
• Khazem K, Tautschnig M (2016), smid: A Black-Box Program Driver $nameOfConference

  
  

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

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

  
  
• Mukherjee R, Tautschnig M, Kroening D (2016), V2c – A Verilog to C translator $nameOfConference

  
  

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

  
  
• 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
• Nellis A, Kesseli P, Conmy PR et al. (2015), Assisted Coverage Closure $nameOfConference

  
  

  DOI: 10.48550/arxiv.1509.04587

  
  
• 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

  
  
• Tautschnig M (2015), CBMC: Bounded model checking of concurrent C programs $nameOfConference

  
  
• Chapman M, Chockler H, Kesseli P et al. (2015), Learning the language of error $nameOfConference

  
  

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

  
  
• 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

  
  
• 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

  
  
• Kroening D, Tautschnig M (2014), CBMC – C Bounded Model Checker $nameOfConference

  
  

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

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

  
  

  DOI: 10.1145/2594291.2594347

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

  
  
• 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
• Alglave J, Maranget L, Tautschnig M (2013), Herding Cats - Modelling, simulation, testing, and data-mining for weak memory $nameOfConference

  
  

  DOI: 10.48550/arxiv.1308.6810

  
  
• 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

  
  

  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

  
  
• 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

  
  

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

  
  
• 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

  
  

  DOI: 10.1109/CSMR.2013.72

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

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

  
  

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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

  
  
• 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

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

  
  

  DOI: 10.1145/1858996.1859084

  
  
• 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

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

  
  

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

  
  
• Langer B, Tautschnig M (2009), Navigating the Requirements Jungle $nameOfConference

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

  
  
• Haberl W, Tautschnig M, Baumgarten U (2009), Generating distributed code from cola models $nameOfConference

  
  

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

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

  
  

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

  
  
• 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

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

  
  

  DOI: 10.1109/ICSTW.2008.1

  
  
• 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

  
  

  DOI: 10.1109/FDL.2008.4641445

  
  
• 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

  
  
• 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

  
  
• Langer B, Tautschnig M (2008), Navigating the Requirements Jungle. $nameOfConference

  
  

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

  
  
• 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

  
  
• 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

  
  

  DOI: 10.1109/EUROMICRO.2007.24

  
  
• 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

  
  

  DOI: 10.1109/DATE.2007.364411