Menu
 
Research menu
Jump to menu

Publications:  Dr Michael Tautschnig

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
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.
10.1007/978-3-319-40648-0_5
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
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 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.
10.1007/978-3-642-54862-8_26
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.
10.1007/978-3-642-37036-6_26
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.
10.4230/LIPIcs.FSTTCS.2013.377
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 Bounded Model Checking of Concurrent Software. CAV. Editors: Sharygina, N, Veith, H, vol. 8044, 141-157.
10.1007/978-3-642-39799-8_9
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.
10.1007/978-3-642-28756-5_5
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.
10.1007/978-3-642-28756-5_43
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.
10.1007/978-3-642-28756-5_47
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.
10.1007/978-3-642-24372-1_3
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.
10.1007/978-3-642-19811-3_20
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.
10.1007/978-3-642-25318-8_21
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.
10.1007/978-3-642-19583-9_5
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.
10.1007/978-3-540-93900-9_15
Gruber H, Holzer M, Tautschnig M (2009) . Short Regular Expressions from Finite Automata: Empirical Results. CIAA. Editors: Maneth, S, vol. 5642, 188-197.
10.1007/978-3-642-02979-0_22
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.
10.1109/FDL.2008.4641445
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.
10.1007/978-3-540-70545-1_20
Langer B, Tautschnig M (2008) . Navigating the Requirements Jungle. ISoLA. Editors: Margaria, T, Steffen, B, vol. 17, 354-368.
10.1007/978-3-540-88479-8_25
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.
10.1007/978-3-540-88479-8_28
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
Alglave J, Maranget L, Tautschnig M. Herding Cats - Modelling, simulation, testing, and data-mining for weak memory.
10.1145/2594291.2594347
http://qmro.qmul.ac.uk/xmlui/handle/123456789/11250
Tautschnig M. Home Page.
Publisher URL
Holzer A, Schallhart C, Tautschnig M et al.. On the Structure and Complexity of Rational Sets of Regular Languages.
http://qmro.qmul.ac.uk/xmlui/handle/123456789/12016
Alglave J, Kroening D, Tautschnig M. Partial Orders for Efficient BMC of Concurrent Software.
http://qmro.qmul.ac.uk/xmlui/handle/123456789/3659
Alglave J, Kroening D, Nimal V et al.. Software Verification for Weak Memory via Program Transformation.
http://qmro.qmul.ac.uk/xmlui/handle/123456789/3679
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