Dr Michael TautschnigLecturerEmail: michael.tautschnig@qmul.ac.ukTelephone: +44 20 7882 5226Room Number: Peter Landin, CS 432Website: http://www.tautschnig.netOffice Hours: Tuesday 13:00-14:30TeachingResearchPublicationsTeachingProgramming 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.ResearchResearch Interests:Software VerificationConcurrencyDecision ProceduresPublications 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 Beyer D, Dangl M, Dietsch D et al. (2022). Verification Witnesses.. nameOfConference DOI: doi QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/101938 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://uat2-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://uat2-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. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice DOI: 10.1145/3377813.3381347 QMRO: https://uat2-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://uat2-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://uat2-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://uat2-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://uat2-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://uat2-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://uat2-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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/11330 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 Nellis A, Kesseli P, Conmy PR et al. (2016). Assisted Coverage Closure.. nameOfConference DOI: doi 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://uat2-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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/13690 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 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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/11032 Kroening D, Liang L, Melham T et al. (publicationYear). Effective verification of low-level software with nested interrupts. Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015 DOI: 10.7873/date.2015.0360 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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/12009 Tautschnig M (2015). CBMC: Bounded model checking of concurrent C programs. nameOfConference DOI: doi QMRO: qmroHref Bloem R, Konighofer R, Rock F et al. (2014). Automating test-suite augmentation. 2014 14th International Conference on Quality Software DOI: 10.1109/qsic.2014.40 QMRO: https://uat2-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 Alglave J, Maranget L, Tautschnig M (2014). Herding cats. nameOfConference DOI: 10.1145/2666356.2594347 QMRO: qmroHref 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 et al. (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 Horn A, Tautschnig M, Val C et al. (publicationYear). Formal co-validation of low-level hardware/software interfaces. 2013 Formal Methods in Computer-Aided Design DOI: 10.1109/fmcad.2013.6679400 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://uat2-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://uat2-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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/3659 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://uat2-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 VV, 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