Publications:  Dr Michael Tautschnig

Khazem K, Tautschnig M (2019). CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker - (Competition Contribution). TACAS (3). Editors: Beyer, D, Huisman, M, Kordon, F, Steffen, B et al., vol. 11429, 199-203.

Cook B, Khazem K, Kroening D, Tasiran S, TAUTSCHNIG M, Tuttle M (2018). Model Checking Boot Code from AWS Data Centers. Conference: Computer Aided Verification

Liang L, Melham T, Kroening D, Schrammel P, TAUTSCHNIG M(2018). Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems vol. 17, 1-26.

Beyer D, Dangl M, Lemberger T, Tautschnig M (2018). Tests from Witnesses - Execution-Based Validation of Verification Results. TAP@STAF. Editors: Dubois, C, Wolff, B, vol. 10889, 3-23.

Huisman M, Klebanov V, Monahan R, Tautschnig M(2017). VerifyThis 2015 A program verification competition. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER vol. 19, (6) 763-771.

Prabhu S, Schrammel P, Srivas MK, Tautschnig M, Yeolekar A (2017). Concurrent Program Verification with Invariant-Guided Underapproximation. ATVA. Editors: D'Souza, D, Kumar, KN, vol. 10482, 241-248.

Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P, Tautschnig M(2016). Assisted Coverage Closure. NASA FORMAL METHODS, NFM 2016 vol. 9690, 49-64.

Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P, Tautschnig M (2016). Assisted Coverage Closure. NFM. Editors: Rayadurgam, S, Tkachuk, O, vol. 9690, 49-64.

Khazem K, Tautschnig M (2016). smid: A Black-Box Program Driver. Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. 182-188.

Mukherjee R, Tautschnig M, Kroening D (2016). v2c - A Verilog to C Translator. Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Conference: Tools and Algorithms for the Construction and Analysis of Systems580-586.

Mukherjee R, Tautschnig M, Kroening D (2016). v2c-A Verilog to C Translator. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016). vol. 9636, 580-586.

Holzer A, Schallhart C, Tautschnig M, Veith H(2015). Closure properties and complexity of rational sets of regular languages. THEORETICAL COMPUTER SCIENCE vol. 605, 62-79.

Kroening D, Liang L, Melham T, Schrammel P, Tautschnig M, IEEE (2015). Effective Verification of Low-Level Software with Nested Interrupts. 2015 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE). 229-234.

Chapman M, Chockler H, Kesseli P, Kroening D, Strichman O, Tautschnig M (2015). Learning the Language of Error. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015. vol. 9364, 114-130.

Alglave J, Maranget L, Tautschnig M(2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS vol. 36, (2) Article ARTN 7,

Alglave J, Maranget L, Tautschnig M (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. ACM SIGPLAN NOTICES. vol. 49, 40-40.

Kroening D, Tautschnig M (2014). Automating Software Analysis at Large Scale. MATHEMATICAL AND ENGINEERING METHODS IN COMPUTER SCIENCE, MEMICS 2014. vol. 8934, 30-39.

Bloem R, Koenighofer R, Roeck F, Tautschnig M, IEEE (2014). Automating Test-Suite Augmentation. 2014 14TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC 2014). 67-72.

Kroening D, Tautschnig M (2014). CBMC - C Bounded Model Checker - (Competition Contribution). TACAS. Editors: Ábrahám, E, Havelund, K, vol. 8413, 389-391.

Alglave J, Maranget L, Tautschnig M(2014). Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. vol. 36, Article 2, 7:1-7:1.

Alglave J, Maranget L, Tautschnig M, ACM (2014). Herding cats: Modelling, simulation, testing, and data-mining for weak memory. PLDI'14: PROCEEDINGS OF THE 2014 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. 40-40.

Beyer D, Holzer A, Tautschnig M, Veith H (2014). Reusing Information in Multi-Goal Reachability Analyses. Software Engineering. Editors: Hasselbring, W, Ehmke, NC, vol. P-227, 97-98.

Horn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J, Kroening D, IEEE (2013). Formal Co-Validation of Low-Level Hardware/Software Interfaces. 2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD). 121-128.

Alglave J, Maranget L, Tautschnig M(2013). Herding Cats. CoRR vol. abs/1308.6810,

Beyer D, Holzer A, Tautschnig M, Veith H (2013). Information Reuse for Multi-goal Reachability Analyses. ESOP. Editors: Felleisen, M, Gardner, P, vol. 7792, 472-491.

Holzer A, Schallhart C, Tautschnig M, Veith H(2013). On the Structure and Complexity of Rational Sets of Regular Languages. CoRR vol. abs/1305.6074,

Holzer A, Schallhart C, Tautschnig M, Veith H (2013). On the Structure and Complexity of Rational Sets of Regular Languages. FSTTCS. Editors: Seth, A, Vishnoi, NK, vol. 24, 377-388.

Chockler H, Denaro G, Ling M, Fedyukovich G, Hyvärinen AEJ, Mariani L, Muhammad A, Oriol M et al. (2013). PINCETTE - Validating Changes and Upgrades in Networked Software. CSMR. Editors: Cleve, A, Ricca, F, Cerioli, M, 461-464.

Alglave J, Kroening D, Tautschnig M(2013). Partial Orders for Efficient BMC of Concurrent Software. CoRR vol. abs/1301.1629,

Alglave J, Kroening D, Tautschnig M (2013). Partial Orders for Efficient Bounded Model Checking of Concurrent Software. CAV. Editors: Sharygina, N, Veith, H, vol. 8044, 141-157.

Alglave J, Kroening D, Nimal V, Tautschnig M(2013). Software Verification for Weak Memory via Program Transformation. PROGRAMMING LANGUAGES AND SYSTEMS vol. 7792, 512-532.

Alglave J, Kroening D, Nimal V, Tautschnig M (2013). Software Verification for Weak Memory via Program Transformation. Proceedings of 22nd European Symposium on Programming. Editors: Felleisen, M, Gardner, P, vol. 7792, 512-532.

Donaldson AF, Kaiser A, Kroening D, Tautschnig M, Wahl T(2012). Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. vol. 41, Article 1, 25-44.

D'Silva V, Haller L, Kroening D, Tautschnig M (2012). Numeric Bounds Analysis with Conflict-Driven Learning. TACAS. Editors: Flanagan, C, König, B, vol. 7214, 48-63.

Holzer A, Kroening D, Schallhart C, Tautschnig M, Veith H (2012). Proving Reachability Using FShell - (Competition Contribution). TACAS. Editors: Flanagan, C, König, B, vol. 7214, 538-541.

Basler G, Donaldson AF, Kaiser A, Kroening D, Tautschnig M, Wahl T (2012). satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). TACAS. Editors: Flanagan, C, König, B, vol. 7214, 552-555.

Bünte S, Zolda M, Tautschnig M, Kirner R (2011). Improving the Confidence in Measurement-Based Timing Analysis. ISORC. 144-151.

Alglave J, Donaldson AF, Kroening D, Tautschnig M (2011). Making Software Verification Tools Really Work. ATVA. Editors: Bultan, T, Hsiung, P-A, vol. 6996, 28-42.

Holzer A, Januzaj V, Kugele S, Langer B, Schallhart C, Tautschnig M, Veith H (2011). Seamless Testing for Models and Code. FASE. Editors: Giannakopoulou, D, Orejas, F, vol. 6603, 278-293.

Alglave J, Kroening D, Lugton J, Nimal V, Tautschnig M (2011). Soundness of Data Flow Analyses for Weak Memory Models. APLAS. Editors: Yang, H, vol. 7078, 272-288.

Holzer A, Tautschnig M, Schallhart C, Veith H (2010). An Introduction to Test Specification in FQL. Haifa Verification Conference. Editors: Barner, S, Harris, IG, Kroening, D, Raz, O et al., vol. 6504, 9-22.

Bauer A, Leucker M, Schallhart C, Tautschnig M(2010). Don't care in SMT: building flexible yet efficient abstraction/refinement solvers. Int. J. Softw. Tools Technol. Transf. vol. 12, Article 1, 23-37.

Holzer A, Schallhart C, Tautschnig M, Veith H (2010). How did you specify your test suite. ASE. Editors: Pecheur, C, Andrews, J, Nitto, ED, 407-416.

Haberl W, Herrmannsdoerfer M, Kugele S, Tautschnig M, Wechs M (2010). Seamless Model-Driven Development Put into Practice. ISoLA (1). Editors: Margaria, T, Steffen, B, vol. 6415, 18-32.

Holzer A, Januzaj V, Kugele S, Tautschnig M (2010). Timely Time Estimates. ISoLA (1). Editors: Margaria, T, Steffen, B, vol. 6415, 33-46.

Holzer A, Schallhart C, Tautschnig M, Veith H (2009). Query-Driven Program Testing. VMCAI. Editors: Jones, ND, Müller-Olm, M, vol. 5403, 151-166.

Gruber H, Holzer M, Tautschnig M (2009). Short Regular Expressions from Finite Automata: Empirical Results. CIAA. Editors: Maneth, S, vol. 5642, 188-197.

Bünte S, Tautschnig M (2008). A Benchmarking Suite for Measurement-Based WCET Analysis Tools. ICST Workshops. 353-356.

Wang Z, Herkersdorf A, Merenda S, Tautschnig M, IEEE (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. 2008 FORUM ON SPECIFICATION, VERIFICATION AND DESIGN LANGUAGES. 221-+.

Wang Z, Herkersdorf A, Merenda S, Tautschnig M (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. FDL. 197-202.

Wang Z, Haberl W, Kugele S, Tautschnig M (2008). Automatic generation of systemc models from component-based designs for early design validation and performance analysis. WOSP. Editors: Avritzer, A, Weyuker, EJ, Woodside, CM, 139-144.

Holzer A, Schallhart C, Tautschnig M, Veith H (2008). FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. CAV. Editors: Gupta, A, Malik, S, vol. 5123, 209-213.

Langer B, Tautschnig M (2008). Navigating the Requirements Jungle. ISoLA. Editors: Margaria, T, Steffen, B, vol. 17, 354-368.

Kugele S, Haberl W, Tautschnig M, Wechs M (2008). Optimizing Automatic Deployment Using Non-functional Requirement Annotations. ISoLA. Editors: Margaria, T, Steffen, B, vol. 17, 400-414.

Haberl W, Tautschnig M, Baumgarten U, ENG IA (2008). Running COLA on embedded systems. IMECS 2008: INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II. 922-928.

Kühnel C, Bauer A, Tautschnig M (2007). Compatibility and reuse in component-based systems via type and unit inference. EUROMICRO-SEAA. 101-108.

Bauer A, Leucker M, Schallhart C, Tautschnig M (2007). Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers. ISoLA. Editors: Ameur, YA, Boniol, F, Wiels, V, vol. RNTI-SM-1, 135-146.

Bauer A, Pister M, Tautschnig M (2007). Tool-support for the analysis of hybrid systems and models. DATE. Editors: Lauwereins, R, Madsen, J, 924-929.