Publications    Interests    Teaching    Michael Tautschnig
michael@tautschnig.net (PGP key)
Michael Tautschnig
Current and recent teaching
 
Publications

  Journal articles and book chapters
 
Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, and Michael Tautschnig. Effective verification for low-level software with competing interrupts. ACM Trans. Embedded Comput. Syst., 17(2):36:1--36:26, 2018. [ bib | DOI | http ]
 
Marieke Huisman, Vladimir Klebanov, Rosemary Monahan, and Michael Tautschnig. Verifythis 2015 - A program verification competition. STTT, 19(6):763--771, 2017. [ bib | DOI | http ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Closure properties and complexity of rational sets of regular languages. Theor. Comput. Sci., 605:62--79, 2015. [ bib | DOI | http ]
 
Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1--7:74, 2014. Cited in Linux Weekly News and C/C++ WG21/4215.bib | DOI | http ]
 
Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design, 41(1):25--44, 2012. [ bib | DOI | http ]
 
Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig. Don't care in SMT---building flexible yet efficient abstraction/refinement solvers. International Journal on Software Tools for Technology Transfer, 12(1):23--37, February 2010. [ bib | DOI ]
 
Wolfgang Haberl, Michael Tautschnig, and Uwe Baumgarten. Generating Distributed Code From COLA Models, volume 33 of Lecture Notes in Electrical Engineering, chapter 20. Springer, March 2009. [ bib ]
 
Wolfgang Haberl, Michael Tautschnig, and Uwe Baumgarten. From COLA Models to Distributed Embedded Systems Code. IAENG International Journal of Computer Science, 35(3):427--437, September 2008. [ bib | pdf ]
  Refereed conference and workshop papers
 
Kareem Khazem and Michael Tautschnig. CBMC path: A symbolic execution retrofit of the C bounded model checker - (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science, pages 199--203. Springer, 2019. [ bib | DOI | http ]
 
Dirk Beyer, Matthias Dangl, Thomas Lemberger, and Michael Tautschnig. Tests from witnesses - execution-based validation of verification results. In Tests and Proofs - 12th International Conference, TAP 2018, Held as Part of STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings, volume 10889 of Lecture Notes in Computer Science, pages 3--23. Springer, 2018. [ bib | DOI | http ]
 
Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Model checking boot code from AWS data centers. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 467--486. Springer, 2018. [ bib | DOI | http ]
 
Sumanth Prabhu, Peter Schrammel, Mandayam K. Srivas, Michael Tautschnig, and Anand Yeolekar. Concurrent program verification with invariant-guided underapproximation. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 241--248. Springer, 2017. [ bib | DOI | http ]
 
Rajdeep Mukherjee, Michael Tautschnig, and Daniel Kroening. v2c - A verilog to C translator. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of Lecture Notes in Computer Science, pages 580--586. Springer, 2016. [ bib | DOI | http ]
 
Kareem Khazem and Michael Tautschnig. smid: A black-box program driver. In 23rd International Symposium on Model Checking Software (SPIN 2016), volume 9641 of Lecture Notes in Computer Science, pages 182--188. Springer, 2016. [ bib | DOI | http ]
 
Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel, and Michael Tautschnig. Assisted coverage closure. In NASA Formal Methods (NFM 2016), volume 9690 of Lecture Notes in Computer Science, pages 49--64. Springer, 2016. [ bib | DOI | http ]
 
Pasquale Malacaria, Michael Tautschnig, and Dino Distefano. Information leakage analysis of complex C code and its application to openssl. In 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), volume 9952 of Lecture Notes in Computer Science, pages 909--925, 2016. [ bib | DOI | http ]
 
Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, and Michael Tautschnig. Learning the language of error. In 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), volume 9364 of Lecture Notes in Computer Science, pages 114--130. Springer, October 2015. [ bib | DOI | http ]
 
Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. Effective verification of low-level software with nested interrupts. In Design, Automation & Test in Europe Conference & Exhibition (DATE 2015), pages 229--234. ACM, March 2015. [ bib | http ]
 
Daniel Kroening and Michael Tautschnig. Automating software analysis at large scale. In 9th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2014), volume 8934 of Lecture Notes in Computer Science, pages 30--39. Springer, October 2014. [ bib | DOI | http ]
 
Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker - (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), volume 8413 of Lecture Notes in Computer Science, pages 389--391. Springer, April 2014. CBMC won the overall Gold medal.bib | DOI | http ]
 
Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith. Reusing information in multi-goal reachability analyses. In Software Engineering 2014, volume 227 of LNI, pages 97--98. GI, 2014. [ bib | http ]
 
Roderick Bloem, Robert Könighofer, Franz Röck, and Michael Tautschnig. Automating test-suite augmentation. In Quality Software (QSIC 2014), pages 67--72. IEEE, 2014. [ bib | DOI | http ]
 
Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: modelling, simulation, testing, and data-mining for weak memory. In Programming Language Design and Implementation (PLDI 2014), page 7. ACM, 2014. [ bib | DOI | http ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. On the structure and complexity of rational sets of regular languages. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), volume 24 of LIPIcs, pages 377--388. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, December 2013. [ bib | DOI | http ]
 
Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, and Daniel Kroening. Formal co-validation of low-level hardware/software interfaces. In Formal Methods in Computer-Aided Design (FMCAD 2013), pages 121--128. IEEE, October 2013. [ bib | http ]
 
Jade Alglave, Daniel Kroening, and Michael Tautschnig. Partial orders for efficient bounded model checking of concurrent software. In Computer Aided Verification (CAV 2013), volume 8044 of Lecture Notes in Computer Science, pages 141--157. Springer, July 2013. [ bib | DOI | http ]
 
Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. Software verification for weak memory via program transformation. In 22nd European Symposium on Programming (ESOP 2013), volume 7792 of Lecture Notes in Computer Science, pages 512--532. Springer, March 2013. [ bib | DOI | http ]
 
Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith. Information reuse for multi-goal reachability analyses. In 22nd European Symposium on Programming (ESOP 2013), volume 7792 of Lecture Notes in Computer Science, pages 472--491. Springer, March 2013. [ bib | DOI | http ]
 
Hana Chockler, Giovanni Denaro, Meijia Ling, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Leonardo Mariani, Ali Muhammad, Manuel Oriol, Ajitha Rajan, Ondrej Sery, Natasha Sharygina, and Michael Tautschnig. PINCETTE -- validating changes and upgrades in networked software. In 17th European Conference on Software Maintenance and Reengineering, (CSMR 2013), pages 461--464. IEEE Computer Society, March 2013. Best paper award.bib | DOI | http ]
 
Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. satabs: A bit-precise verifier for C programs - (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), volume 7214 of Lecture Notes in Computer Science, pages 552--555. Springer, April 2012. [ bib | DOI | http ]
 
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Proving reachability using FShell - (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), volume 7214 of Lecture Notes in Computer Science, pages 538--541. Springer, April 2012. [ bib | DOI | http ]
 
Vijay D'Silva, Leopold Haller, Daniel Kroening, and Michael Tautschnig. Numeric bounds analysis with conflict-driven learning. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), volume 7214 of Lecture Notes in Computer Science, pages 48--63. Springer, April 2012. [ bib | DOI | http ]
 
Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, and Michael Tautschnig. Soundness of data flow analyses for weak memory models. In i9th Asian Symposium of Programming Languages and Systems (APLAS 2011), volume 7078 of Lecture Notes in Computer Science, pages 272--288. Springer, December 2011. [ bib | DOI | http ]
 
Jade Alglave, Alastair F. Donaldson, Daniel Kroening, and Michael Tautschnig. Making software verification tools really work. In Automated Technology for Verification and Analysis (ATVA 2011), volume 6996 of Lecture Notes in Computer Science, pages 28--42. Springer, October 2011. [ bib ]
 
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Seamless testing for models and code. In 14th International Conference on Fundamental Approaches to Software Engineering (FASE 2011), volume 6603 of Lecture Notes in Computer Science, pages 278--293. Springer, April 2011. [ bib ]
 
Sven Bünte, Michael Zolda, Michael Tautschnig, and Raimund Kirner. Improving the confidence in measurement-based timing analysis. In 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, ISORC 2011, pages 144--151. IEEE Computer Society, March 2011. [ bib ]
 
Andreas Holzer, Visar Januzaj, Stefan Kugele, and Michael Tautschnig. Timely time estimates. In 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2010), volume 6415 of Lecture Notes in Computer Science, pages 33--46. Springer, October 2010. [ bib | DOI ]
 
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs. Seamless model-driven development put into practice. In 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2010), volume 6415 of Lecture Notes in Computer Science, pages 18--32, Heraklion, Crete, Greece, October 2010. Springer. [ bib | DOI ]
 
Andreas Holzer, Michael Tautschnig, Christian Schallhart, and Helmut Veith. An introduction to test specification in FQL. In 6th International Haifa Verification Conference (HVC 2011), volume 6504 of Lecture Notes in Computer Science, pages 9--22. Springer, October 2010. [ bib ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. How did you specify your test suite ? In Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), pages 407--416. ACM, September 2010. [ bib | DOI ]
 
Hermann Gruber, Markus Holzer, and Michael Tautschnig. Short regular expressions from finite automata: Empirical results. In 14th International Conference on Implementation and Application of Automata (CIAA 2009), volume 5642 of Lecture Notes in Computer Science, pages 188--197. Springer, July 2009. [ bib ]
 
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs. One click from model to reality. In Proceedings of Symposium on Automotive/Avionics Systems Engineering (SAASE 2009), 2009. [ bib ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Query-driven program testing. In Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), volume 5403 of Lecture Notes in Computer Science, pages 151--166. Springer, January 2009. [ bib | DOI | pdf ]
 
Stefan Kugele, Wolfgang Haberl, Michael Tautschnig, and Martin Wechs. Optimizing automatic deployment using non-functional requirement annotations. In Leveraging Applications of Formal Methods, Verification and Validation, volume 17 of Communications in Computer and Information Science, pages 400--414. Springer, October 2008. [ bib ]
 
Boris Langer and Michael Tautschnig. Navigating the requirements jungle. In Leveraging Applications of Formal Methods, Verification and Validation, volume 17 of Communications in Computer and Information Science, pages 354--368. Springer, October 2008. [ bib | pdf ]
 
Zhonglei Wang, Andreas Herkersdorf, Stefano Merenda, and Michael Tautschnig. A model driven development approach for implementing reactive systems in hardware. In Forum on Specification and Design Languages (FDL08), pages 197--202. IEEE Computer Society, September 2008. [ bib | DOI ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. In 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, pages 209--213. Springer, July 2008. [ bib | DOI | pdf ]
 
Zhonglei Wang, Wolfgang Haberl, Stefan Kugele, and Michael Tautschnig. Automatic generation of systemc models from component-based designs for early design validation and performance analysis. In 7th International Workshop on Software and Performance (WOSP 2008), pages 139--144. ACM, June 2008. [ bib | pdf ]
 
Sven Bünte and Michael Tautschnig. A benchmarking suite for measurement-based WCET analysis tools. In International Conference on Software Testing Verification and Validation Workshop (ICSTW'08), pages 353--356. IEEE Computer Society Press, April 2008. [ bib | DOI | pdf ]
 
Wolfgang Haberl, Michael Tautschnig, and Uwe Baumgarten. Running COLA on Embedded Systems. In Proceedings of The International MultiConference of Engineers and Computer Scientists 2008, pages 922--928, Hongkong, China, March 2008. Awarded Certificate of Merit.bib | pdf ]
 
Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig. Don't care in SMT---building flexible yet efficient abstraction/refinement solvers. In 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 135--146, Poitiers, France, December 2007. [ bib | pdf ]
 
Christian Kühnel, Andreas Bauer, and Michael Tautschnig. Compatibility and reuse in component-based systems via type and unit inference. In Proceedings of the 33rd EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pages 101--108. IEEE Computer Society Press, August 2007. [ bib | DOI | pdf ]
 
Andreas Bauer, Markus Pister, and Michael Tautschnig. Tool-support for the analysis of hybrid systems and models. In 2007 Conference on Design, Automation and Test in Europe (DATE 2007), pages 924--929. European Design and Automation Association, April 2007. [ bib | DOI | pdf ]
  Talks
 
Michael Tautschnig. FQL: A Query Language for Program Testing. Joint meeting of Quality Software Engineering and FORSYTE groups, March 2010. talk. [ bib ]
 
Michael Tautschnig. FQL: A Query Language for Program Testing. IST / TU Rigorous Systems Engineering Seminar, March 2010. talk. [ bib ]
 
Michael Tautschnig. Tools for Concurrency and Distributed Systems. RiSE Workshop, February 2010. talk. [ bib ]
 
Michael Tautschnig. FQL: A Query Language for Program Testing. Joint meeting of Tom Henzinger's group and FORSYTE, January 2010. talk. [ bib ]
 
Michael Tautschnig. FQL: A Query Language for Program Testing. 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'09), October 2009. talk. [ bib ]
 
Michael Tautschnig. Query-Driven Program Testing. Joint meeting of groups from Oxford, ETH Zürich, and FORSYTE, April 2009. talk. [ bib ]
 
Michael Tautschnig. FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. Alpine Verification Meeting, May 2008. talk. [ bib ]
 
Michael Tautschnig. A Query Language for Programs. i7@Bodenmais, July 2007. talk. [ bib ]
 
Michael Tautschnig. Satisfiability Modulo Theories: ABsolver. Joint meeting DTU-TUM, May 2007. talk. [ bib | pdf ]
  Technical reports
 
Andreas Holzer, Visar Januzaj, Stefan Kugele, Christian Schallhart, Michael Tautschnig, Helmut Veith, and Boris Langer. Slope testing for activity diagrams and safety critical software. Technical Report TUD-CS-2009-0184, Technische Universität Darmstadt, October 2009. [ bib ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. A precise specification framework for white box program testing. Technical Report TUD-CS-2009-0148, Technische Universität Darmstadt, September 2009. [ bib ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Dependency coverage criteria with FQL. Technical Report TUD-CS-2009-0149, Technische Universität Darmstadt, 2009. [ bib ]
 
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Query-driven program testing. Technical Report TUD-CS-2008-1013, Technische Universität Darmstadt, October 2008. [ bib ]
 
Stefan Kugele, Michael Tautschnig, Andreas Bauer, Christian Schallhart, Stefano Merenda, Wolfgang Haberl, Christian Kühnel, Florian Müller, Zhonglei Wang, Doris Wild, Sabine Rittmann, and Martin Wechs. COLA -- the component language. Technical Report TUM-I0714, Institut für Informatik, Technische Universität München, September 2007. [ bib | pdf ]
 
Christian Kühnel, Andreas Bauer, and Michael Tautschnig. Compatibility and reuse in component-based systems via type and unit inference. Technical Report TUM-I0716, Institut für Informatik, Technische Universität München, May 2007. [ bib | pdf ]
  Theses
 
Michael Tautschnig. Query-Driven Program Testing. PhD thesis, Vienna University of Technology, 2011. [ bib | pdf ]
 
Michael Tautschnig. Development of a tool to solve mixed logical/linear constraint problems. Master's thesis, Technische Universität München, February 2006. [ bib | pdf ]

Generated by bibtex2html 1.99.


ACM, Springer-Verlag, and IEEE-mandated Copyright Notice
The documents listed above are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder. ACM, Springer-Verlag, and IEEE published documents have other restrictions given here, here, and here.
My curriculum vitae

Programming today is a race between software engineers striving to build bigger and better idiot-proof programs, and the Universe trying to produce bigger and better idiots. So far, the Universe is winning.

Research interests
  • Improving software quality
  • Model Checking
  • Testing
  • Concurrency
  • Constraint solvers
  • Embedded systems

I'm interested in free software and try to contribute to some open source software projects, whenever time permits.
Publications    Interests    Teaching        Valid HTML 4.01 Strict Valid CSS!
To me vi is Zen. To use vi is to practice Zen. Every command is a koan. Profound to the user, unintelligible to the uninitiated. You discover truth every time you use it.