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.