Menu
 
Research menu
Jump to menu

Publications:  Dr Michael Tautschnig

Cook B, Khazem K, Kroening D et al. (2018). Model Checking Boot Code from AWS Data Centers. Conference: Computer Aided Verification
http://qmro.qmul.ac.uk/xmlui/handle/123456789/44645
Liang L, Melham T, Kroening D et al.(2018). Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems vol. 17, 1-26.
10.1145/3147432
http://qmro.qmul.ac.uk/xmlui/handle/123456789/31940
Beyer D, Dangl M, Lemberger T et al. (2018). Tests from Witnesses - Execution-Based Validation of Verification Results. TAP. Editors: Dubois, C, Wolff, B, vol. 10889, 3-23.
Huisman M, Klebanov V, Monahan R et al.(2017). VerifyThis 2015 A program verification competition. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER vol. 19, (6) 763-771.
10.1007/s10009-016-0438-x
http://qmro.qmul.ac.uk/xmlui/handle/123456789/31939
Prabhu S, Schrammel P, Srivas MK et al. (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 et al.(2016). Assisted Coverage Closure. NASA FORMAL METHODS, NFM 2016 vol. 9690, 49-64.
10.1007/978-3-319-40648-0_5
http://qmro.qmul.ac.uk/xmlui/handle/123456789/11330
Nellis A, Kesseli P, Conmy PR et al. (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.
10.1007/978-3-319-32582-8_12
http://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 - 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.
10.1007/978-3-662-49674-9_38
http://qmro.qmul.ac.uk/xmlui/handle/123456789/13690
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.
10.1007/978-3-662-49674-9_38
Holzer A, Schallhart C, Tautschnig M et al.(2015). Closure properties and complexity of rational sets of regular languages. THEORETICAL COMPUTER SCIENCE vol. 605, 62-79.
10.1016/j.tcs.2015.08.035
http://qmro.qmul.ac.uk/xmlui/handle/123456789/11032
Kroening D, Liang L, Melham T et al. (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 et al. (2015). Learning the Language of Error. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015. vol. 9364, 114-130.
10.1007/978-3-319-24953-7_9
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,
10.1145/2627752
http://qmro.qmul.ac.uk/xmlui/handle/123456789/11250
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.
10.1145/2594291.2594347
Kroening D, Tautschnig M (2014). Automating Software Analysis at Large Scale. MATHEMATICAL AND ENGINEERING METHODS IN COMPUTER SCIENCE, MEMICS 2014. vol. 8934, 30-39.
10.1007/978-3-319-14896-0_3
http://qmro.qmul.ac.uk/xmlui/handle/123456789/12009
Bloem R, Koenighofer R, Roeck F et al. (2014). Automating Test-Suite Augmentation. 2014 14TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC 2014). 67-72.
10.1109/QSIC.2014.40
http://qmro.qmul.ac.uk/xmlui/handle/123456789/11249
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.
10.1145/2627752
Alglave J, Maranget L, Tautschnig M et al. (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.
10.1145/2594291.2594347
Beyer D, Holzer A, Tautschnig M et al. (2014). Reusing Information in Multi-Goal Reachability Analyses. Software Engineering. Editors: Hasselbring, W, Ehmke, NC, vol. 227, 97-98.
Horn A, Tautschnig M, Val C et al. (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 et al. (2013). Information Reuse for Multi-goal Reachability Analyses. ESOP. Editors: Felleisen, M, Gardner, P, vol. 7792, 472-491.
Holzer A, Schallhart C, Tautschnig M et al.(2013). On the Structure and Complexity of Rational Sets of Regular Languages. CoRR vol. abs/1305.6074,
http://qmro.qmul.ac.uk/xmlui/handle/123456789/12016
Holzer A, Schallhart C, Tautschnig M et al. (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 et al. (2013). PINCETTE - Validating Changes and Upgrades in Networked Software. CSMR. Editors: Cleve, A, Ricca, F, Cerioli, M, 461-464.
10.1109/CSMR.2013.72
Alglave J, Kroening D, Tautschnig M(2013). Partial Orders for Efficient BMC of Concurrent Software. CoRR vol. abs/1301.1629,
http://qmro.qmul.ac.uk/xmlui/handle/123456789/3659
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 et al.(2013). Software Verification for Weak Memory via Program Transformation. PROGRAMMING LANGUAGES AND SYSTEMS vol. 7792, 512-532.
http://qmro.qmul.ac.uk/xmlui/handle/123456789/3679
Alglave J, Kroening D, Nimal V et al. (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.
10.1007/978-3-642-37036-6_28
Donaldson AF, Kaiser A, Kroening D et al.(2012). Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design vol. 41, Article 1, 25-44.
10.1007/s10703-012-0155-3
D'Silva V, Haller L, Kroening D et al. (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 et al. (2012). Proving Reachability Using FShell - (Competition Contribution). TACAS. Editors: Flanagan, C, König, B, vol. 7214, 538-541.
Basler G, Donaldson AF, Kaiser A et al. (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 et al. (2011). Improving the Confidence in Measurement-Based Timing Analysis. ISORC. 144-151.
10.1109/ISORC.2011.27
Alglave J, Donaldson AF, Kroening D et al. (2011). Making Software Verification Tools Really Work. ATVA. Editors: Bultan, T, Hsiung, P-A, vol. 6996, 28-42.
Holzer A, Januzaj V, Kugele S et al. (2011). Seamless Testing for Models and Code. FASE. Editors: Giannakopoulou, D, Orejas, F, vol. 6603, 278-293.
Alglave J, Kroening D, Lugton J et al. (2011). Soundness of Data Flow Analyses for Weak Memory Models. APLAS. Editors: Yang, H, vol. 7078, 272-288.
Holzer A, Tautschnig M, Schallhart C et al. (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 et al.(2010). Don't care in SMT: building flexible yet efficient abstraction/refinement solvers. STTT vol. 12, Article 1, 23-37.
10.1007/s10009-009-0133-2
Holzer A, Schallhart C, Tautschnig M et al. (2010). How did you specify your test suite. ASE. Editors: Pecheur, C, Andrews, J, Nitto, ED, 407-416.
10.1145/1858996.1859084
Haberl W, Herrmannsdoerfer M, Kugele S et al. (2010). Seamless Model-Driven Development Put into Practice. ISoLA (1). Editors: Margaria, T, Steffen, B, vol. 6415, 18-32.
10.1007/978-3-642-16558-0_4
Holzer A, Januzaj V, Kugele S et al. (2010). Timely Time Estimates. ISoLA (1). Editors: Margaria, T, Steffen, B, vol. 6415, 33-46.
10.1007/978-3-642-16558-0_5
Holzer A, Schallhart C, Tautschnig M et al. (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.
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. 2008 FORUM ON SPECIFICATION, VERIFICATION AND DESIGN LANGUAGES. 221-+.
Wang Z, Herkersdorf A, Merenda S et al. (2008). A Model Driven Development Approach for Implementing Reactive Systems in Hardware. FDL. 197-202.
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. WOSP. Editors: Avritzer, A, Weyuker, EJ, Woodside, CM, 139-144.
10.1145/1383559.1383577
Holzer A, Schallhart C, Tautschnig M et al. (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 et al. (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 et al. (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.
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. 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.
10.1109/DATE.2007.364411
Khazem K, TAUTSCHNIG M. smid: A Black-Box Program Driver. Conference: 23rd International SPIN Symposium on Model Checking of Software
10.1007/978-3-662-49674-9_38
http://qmro.qmul.ac.uk/xmlui/handle/123456789/13960
Return to top