Skip to main content
Research
  1. Queen Mary University of London
  2. Research
  3. Publications

Publications: Dr Michael Tautschnig

Back to Search
Beyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T, Tautschnig M ( 2022 ) . Verification Witnesses . ACM Transactions on Software Engineering and Methodology vol. 31 , ( 4 )
Chong N, Cook B, Eidelman J, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S et al. ( 2021 ) . Code-level model checking in the software development workflow at Amazon Web Services . Software - Practice and Experience vol. 51 , ( 4 ) 772 - 797 .
Cook B, Döbel B, Kroening D, Manthey N, Pohlack M, Polgreen E, Tautschnig M, Wieczorkiewicz P ( 2020 ) . Using model checking tools to triage the severity of security bugs in the Xen hypervisor . Conference: Formal Methods in Computer Aided Design vol. 00 , 185 - 193 .
Chong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M et al. ( 2020 ) . Code-level model checking in the software development workflow . Conference: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice11 - 20 .
Beyer D, Dangl M, Lemberger T, Tautschnig M ( 2019 ) . Tests from Witnesses Execution-Based Validation of Verification Results . TESTS AND PROOFS, TAP 2018 . Conference: Tests and Proofs vol. 10889 , 3 - 23 .
Khazem K, Tautschnig M ( 2019 ) . CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker . Tools and Algorithms for the Construction and Analysis of Systems , vol. 11429 , Springer Nature
Khazem K, Tautschnig M ( 2019 ) . CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution) . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 11429 LNCS , 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
Beyer D, Dangl M, Lemberger T, Tautschnig M ( 2018 ) . Tests from Witnesses . Tests and Proofs , vol. 10889 , Springer Nature
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 .
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 M, Tautschnig M, Yeolekar A ( 2017 ) . Concurrent Program Verification with Invariant-Guided Underapproximation . Conference: Automated Technology for Verification and Analysis vol. 10482 , 241 - 248 .
MALACARIA P, TAUTCHNING M, DISTEFANO D ( 2016 ) . Information leakage analysis of complex C code and its application to OpenSSL . Conference: 7th International Symposium on Leveraging Applications ( CORFU ) from: 10/10/2016 to: 14/10/2016 ,
Nellis A, Kesseli P, Conmy PR, Kroening D, Schrammel P, Tautschnig M ( 2016 ) . Assisted Coverage Closure . NASA Formal Methods vol. 9690 , 49 - 64 .
Mukherjee R, Tautschnig M, Kroening D ( 2016 ) . v2c – A Verilog to C Translator . vol. 9636 , 580 - 586 .
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 .
Chapman M, Chockler H, Kesseli P, Kroening D, Strichman O, Tautschnig M ( 2015 ) . Learning the Language of Error . vol. 9364 , 114 - 130 .
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 . Effective verification of low-level software with nested interrupts . 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE) . Conference: Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015229 - 234 .
Kroening D, Tautschnig M ( 2014 ) . Automating Software Analysis at Large Scale . vol. 8934 , 30 - 39 .
Tautschnig M ( 2015 ) . CBMC: Bounded model checking of concurrent C programs . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 9232 , 11 - 12 .
Bloem R, Konighofer R, Rock F, Tautschnig M ( 2014 ) . Automating test-suite augmentation . Conference: 2014 14th International Conference on Quality Software67 - 72 .
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 7 , 1 - 74 .
Alglave J, Maranget L, Tautschnig M ( 2014 ) . Herding cats . ACM SIGPLAN Notices . vol. 49 , 40 - 40 .
Kroening D, Tautschnig M ( 2014 ) . CBMC - C Bounded Model Checker (Competition contribution) . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 8413 LNCS , 389 - 391 .
Kroening D, Tautschnig M ( 2014 ) . CBMC – C Bounded Model Checker . Tools and Algorithms for the Construction and Analysis of Systems , vol. 8413 , Springer Nature
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 . Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI) . vol. P227 , 97 - 98 .
Horn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J, Kroening D . Formal co-validation of low-level hardware/software interfaces . Conference: 2013 Formal Methods in Computer-Aided Design121 - 128 .
Alglave J, Maranget L, Tautschnig M ( 2013 ) . Herding Cats - Modelling, simulation, testing, and data-mining for weak memory .
Holzer A, Schallhart C, Tautschnig M, Veith H ( 2013 ) . On the Structure and Complexity of Rational Sets of Regular Languages .
Alglave J, Kroening D, Tautschnig M ( 2013 ) . Partial Orders for Efficient BMC of Concurrent Software .
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 . 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 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 . Proceedings of 22nd European Symposium on Programming . Editors: Felleisen, M, Gardner, P , vol. 7792 , 512 - 532 .
Alglave J, Kroening D, Nimal V, Tautschnig M ( 2012 ) . Software Verification for Weak Memory via Program Transformation .
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 VV, 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 . Tools and Algorithms for the Construction and Analysis of Systems , vol. 7214 , Springer Nature
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 A, Kaiser A, Kroening D, Tautschnig M, Wahl T ( 2012 ) . satabs: A Bit-Precise Verifier for C Programs . Tools and Algorithms for the Construction and Analysis of Systems , vol. 7214 , Springer Nature
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 .
Langer B, Tautschnig M ( 2009 ) . Navigating the Requirements Jungle . Communications in Computer and Information Science vol. 17 , 354 - 368 .
Kugele S, Haberl W, Tautschnig M, Wechs M ( 2009 ) . Optimizing Automatic Deployment Using Non-functional Requirement Annotations . Communications in Computer and Information Science vol. 17 , 400 - 414 .
Haberl W, Tautschnig M, Baumgarten U ( 2009 ) . Generating Distributed Code from Cola Models . Trends in Communication Technologies and Engineering Science , vol. 33 , Springer Nature
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 ( 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 ( 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 .
Back to Search