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.
|