GRK 1480:  PUMA Programm- und Modell-Analyse

• Fachliche Zuordnung: Informatik
• Förderung: Förderung von 2008 bis 2017
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 47140942

• Erstellungsjahr: 2018

Zusammenfassung der Projektergebnisse

Die Hauptaufgabe der Programm- und Modell-Analyse ist das Aufdecken von Fehlern bzw. der Nachweis, dass ein Programm oder Modell korrekt ist, d.h. sich gemäß seiner Spezifikation verhält. Eine solche Spezifikation kann etwa verlangen, dass Verklemmungen von Threads oder Laufzeitfehler wie illegale Speicherzugriffe nicht vorkommen. Sie könnte aber auch genaue Vorgaben über den Ressourcenverbrauch oder das Ein/Ausgabe-Verhalten machen. Ausgangspunkt der Forschung im Graduiertenkolleg PUMA sind die vier gängigen Ansätze zur Lösung solcher Probleme: Programm-Verifikation durch Theorembeweisen, Model Checking, Statische Analyse durch Abstrakte Interpretation und Typsysteme. Die tragende Hypothese des Graduiertenkollegs war, dass diese Ansätze, obwohl sie traditionellerweise von unterschiedlichen Communities verfolgt werden, nur scheinbar unvereinbar sind, dass vielmehr die Interaktion, der Austausch zwischen diesen Herangehensweisen zu neuen, möglicherweise besseren Verfahren führen würde. Diese Annahme hat sich im Laufe der ersten drei Jahre und nicht zuletzt durch die Beiträge des Graduiertenkollegs bestätigt: seitdem entwickelt sich die Forschung weltweit in diese Richtung. Das Zusammenwachsen von logischen Entscheidungsprozeduren, Model Checking und abstrakter Interpretation hat sich mittlerweile als eine Einheit etabliert. Der bei Microsoft Research entwickelte SMT-Solver Z3 wird mittlerweile in vielen Werkzeugen für Model Checking, Testing, und Programmanalyse als Back-End eingesetzt. Die Wiederbelebung der Hoarelogik durch Automatisierung und begleitende abstrakte Interpretation hat sich fortgesetzt. Das Ziel des Graduiertenkollegs der ersten Periode, Möglichkeiten zur Kombination der vier Ansätze der Programm- und Modellanalyse auszuloten, wurde deshalb für die zweite Förderperiode verfeinert. Bei einer Logik-basierten Formulierung der Programm- und Modellanalyse ist eine Verbesserung der Entscheidungsprozeduren und Löser von essentieller Bedeutung. Die Constraint-Lösungsalgorithmen aus der ersten Periode wurden deshalb in der zweiten Periode aufgegriffen und weiter verallgemeinert. Neue besser korrekt zu beweisende Verfahren wurden für MSO entwickelt. Ganz neu traten Löser für gewöhnliche Differentialgleichungen in den Fokus des Interesses, da mit ihnen verifizierte Erreichbarkeitsanalysen für cyber-physikalische Systeme konstruiert werden können. Ebenfalls aufgegriffen wurde das Konzept generischer lokaler Fixpunktalgorithmen, die um die Möglichkeit, mit Widening und Narrowing umzugehen, erweitert wurden. Solche Algorithmen bilden das Herz praktischer Programmanalysesysteme. Entscheidende Fortschritte gab es auch in der zweiten Förderperiode bei probabilistischem Model Checking, für das in der ersten Periode verifizierte Implementierungen geliefert wurden. Hier wurden ganz neue und besser skalierende Verfahren gefunden. Ebenfalls in der zweiten Periode weiter geführt wurden die Untersuchung der neuen typbasiertem Techniken zur Analyse des Speicherplatzverbrauchs. Konnten in der ersten Periode Methoden für funktionale, objektorientierte und reaktive Programmiersprachen entwickelt werden, so blieb doch die Lösbarkeit der bei der Analyse objektorienter Programme auftretenden Constraint Systeme offen. Hier konnte erst in der zweiten Förderperiode nachgewiesen werden, dass diese tatsächlich entscheidbar sind. Ein besonderes Highlight in der ersten Periode war die Realisierung eines Werkzeugs zur automatischen Lösung von Syntheseproblemen für Kontrolleinheiten von industriellen Automatisierungsprozessen. In der zweiten Periode dienten autonome Systeme als ein praktisch relevantes Anwendungsszenario. Dieses erwies sich als sehr fruchtbar, da es das Erfordernis einer Formalisierung von Verkehrsregeln mit sich brachte und zu einer Untersuchung von beweisbar sicherem Fahrzeugverhalten anregte.

Projektbezogene Publikationen (Auswahl)

• “Modeling and Verification of Reliable Messaging by Graph Transformation Systems”. In: Proc. of the Workshop on Graph Transformation for Verification and Concurrency (GTVC2006). Elsevier, 2006
  László Gönczy, Máté Kovács, Dániel Varró
  (Siehe online unter https://doi.org/10.1016/j.entcs.2007.04.015)
• “Simulation and Formal Analysis of Workflow Models”. In: Proc. of the Fifth International Workshop on Graph Transformation and Visual Modeling Techniques. Ed. by Roberto Bruni and Daniel Varro. Electronic Notes in Theoretical Computer Science. Vienna, AU- STRIA: Elsevier, 2006, pp. 215–224
  Kovács, Máté; Gönczy, László
  (Siehe online unter https://doi.org/10.1016/j.entcs.2008.04.044)
• “Formal Modeling of BPEL Workflows Including Fault and Compensation Handling”. In: Proc. of the 2007 Workshop on Engineering Fault Tolerant Systems (EFTS 2007). Dubrovnik, Croatia, Sept. 2007
  Kovács, Máté; Varró, Dániel; Gönczy, László
  (Siehe online unter https://doi.org/10.1145/1316550.1316551)
• “An Integrated Framework for the Dependability Evaluation of Distributed Mobile Applications”. In: (SERENE 2008), RISE/EFTS Joint International Workshop on Software Engineering for REsilient SystEms. Newcastle Upon Tyne, UK, Nov. 2008, pp. 29–38
  Kovács, Máté; Lollini, Paolo; Majzik, István; Bondavalli, Andrea
  (Siehe online unter https://doi.org/10.1145/1479772.1479778)
• “Formal analysis of BPEL. workflows with compensation by model checking”. In: Comput. Syst. Sci. Eng. 23.5 (2008)
  Kovács, Máté; Varró, Dániel; Gönczy, László
  
• “Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning”. In: Logical Methods in Computer Science 4.4 (2008)
  Samuel R. Buss, Jan Hoffmann, and Jan Johannsen
  (Siehe online unter https://doi.org/10.2168/LMCS-4(4:13)2008)
• “Syntactic Metatheory of Higher-Order Subtyping”. In: Computer Science Logic, 22nd International Workshop, CSL 2008. Ed. by Michael Kaminski and Simone Martini. LNCS 5213, Springer, 2008, pp. 446–460
  Andreas Abel and Dulma Rodriguez
  (Siehe online unter https://doi.org/10.1007/978-3-540-87531-4_32)
• “The NP-hardness of Finding a Directed Acyclic Graph for Regular Resolution”. In: Theoretical Computer Science 396.1-3 (2008)
  Samuel R. Buss and Jan Hoffmann
  (Siehe online unter https://doi.org/10.1016/j.tcs.2008.01.039)
• “An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it”. In: 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009. 2009, pp. 145–156
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.1109/LICS.2009.27)
• “Comparison of Algorithms for Checking Emptiness on Büchi Automata”. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS). Ed. by Petr Hlinený, Václav Matyás, and Tomás Vojnar. Vol. 13. OASICS. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009
  Andreas Gaiser and Stefan Schwoon
  (Siehe online unter https://doi.org/10.4230/DROPS.MEMICS.2009.2349)
• “Computing Shapley’s saddles”. In: SIGecom Exchanges 8.2 (2009), p. 3
  Felix Brandt, Markus Brill, Felix A. Fischer, Paul Harrenstein, and Jan Hoffmann
  (Siehe online unter https://doi.acm.org/10.1145/1980522.1980525)
• “Examining robotic systems with shape-adjustable manipulators under dynamic environments: From simulation to verification”. In: IEEE International Symposium on Computational Intelligence in Robotics and Automation (CIRA’09). IEEE Computer Society, 2009, pp. 72–77
  Chih-Hong Cheng, Alois Knoll, Christian Buckl, Javier Esparza, and Yang Chen
  (Siehe online unter https://doi.org/10.1109/CIRA.2009.5423243)
• “Efficient Type-Checking for Amortised Heap-Space Analysis”. In: Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL. Ed. by Erich Gr¨adel and Reinhard Kahle. LNCS 5771, Springer, 2009, pp. 317–331
  Martin Hofmann and Dulma Rodriguez
  (Siehe online unter https://doi.org/10.1007/978-3-642-04027-6_24)
• “Finding a Tree Structure in a Resolution Proof is NP- Complete”. In: Theoretical Computer Science 410.21-23 (2009)
  Jan Hoffmann
  (Siehe online unter https://doi.org/10.1016/j.tcs.2009.02.018)
• “InvGen: An Efficient Invariant Generator”. In: Computer Aided Verification, 21st International Conference, CAV 2009. Ed. by Ahmed Bouajjani and Oded Maler. LNCS 5643, Springer, 2009, pp. 634–640
  Ashutosh Gupta and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-02658-4_48)
• “Membership Checking in Greatest Fixpoints Revisited”. In: 6th Workshop on Fixed Points in Computer Science, FICS 2009. Institute of Cybernetics, 2009, pp. 46–53
  Martin Hofmann and Dulma Rodriguez
  
• “On least fixed points of systems of positive polynomials”. In: ACM Comm. Computer Algebra 43.3/4 (2009), pp. 81–83
  Javier Esparza, Andreas Gaiser, and Stefan Kiefer
  (Siehe online unter https://doi.org/10.1145/1823931.1823939)
• “Proof pearl: Mechanizing the textbook proof of Huffman’s algorithm in Isabelle/HOL”. In: J. Autom. Reasoning 43.1 (2009), pp. 1–18
  Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.1007/s10817-009-9116-y)
• “Proving Inequalities over Reals with Computation in Isabelle/HOL”. In: ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS’09). Ed. by Gabriel Dos Reis and Laurent Théry. Munich, Aug. 2009, pp. 38–45
  Johannes Hölzl
  
• “Solving Parity Games in Practice”. In: Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009. 2009, pp. 182–196
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-04761-9_15)
• “The Computational Complexity of Weak Saddles”. In: Algorithmic Game Theory, Second International Symposium, SAGT 2009. Ed. by Marios Mavronicolas and Vicky G. Papadopoulou. LNCS 5814, Springer, 2009, pp. 238–249
  Felix Brandt, Markus Brill, Felix A. Fischer, and Jan Hoffmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-04645-2_22)
• “Turning Inductive into Equational Specifications”. In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009. LNCS 5674, Springer, 2009, pp. 131–146
  Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-03359-9_1)
• "Computing Least Fixed Points of Probabilistic Systems of Polynomials”. In: 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010. Ed. by Jean-Yves Marion and Thomas Schwentick. Vol. 5. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010, pp. 359–370
  Javier Esparza, Andreas Gaiser, and Stefan Kiefer
  (Siehe online unter https://doi.org/10.4230/LIPIcs.STACS.2010.2468)
• Christian Kern and Javier Esparza. “Automatic Error Correction of Java Programs”. In: Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010. LNCS 6371, Springer, 2010, pp. 67–81
  Christian Kern and Javier Esparza
  (Siehe online unter https://doi.org/10.1007/978-3-642-15898-8_5)
• Specifying and verifying sparse matrix codes”. In: 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010. ACM, 2010, pp. 249–260
  Arnold, Gilad; Hölzl, Johannes; Köksal, Ali Sinan; Bodík, Rastislav; Sagiv, Mooly
  (Siehe online unter https://doi.org/10.1145/1863543.1863581)
• “A CTL-Based Logic for Program Abstractions”. In: 17th Workshop on Logic, Language, Information and Computation (WoLLIC 2010, Brasília, Brazil). Ed. by Anuj Dawar and Ruy de Queiroz. LNCS 6188, Springer, 2010, pp. 19–33. isbn: 978-3-642-13823-2
  Martin Lange and Markus Latte
  (Siehe online unter https://doi.org/10.1007/978-3-642-13824-9_2)
• “A Decision Procedure for CTL* Based on Tableaux and Automata”. In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010. LNCS 6173, Springer, 2010, pp. 331–345
  Oliver Friedmann, Markus Latte, and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-14203-1_28)
• “A Solver for Modal Fixpoint Logics”. In: Electr. Notes Theor. Comput. Sci. 262 (2010), pp. 99–111
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1016/j.entcs.2010.04.008)
• “Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics”. In: Programming Languages and Systems - 8th Asian Symposium, APLAS 2010. Ed. by Kazunori Ueda. LNCS 6461, Springer, 2010, pp. 172–187
  Jan Hoffmann and Martin Hofmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-17164-2_13)
• “Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs”. In: Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010. Ed. by Andrew D. Gordon. LNCS 6012, Springer, 2010, pp. 287–306
  Jan Hoffmann and Martin Hofmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-11957-6_16)
• “Bottom-Up Tree Automata with Term Constraints”. In: Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17. Ed. by Christian G. Fermüller and Andrei Voronkov. LNCS 6397, Springer, 2010, pp. 581–593
  Andreas Reuß and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-16242-8_41)
• “Extended Computation Tree Logic”. In: 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR 2010. Ed. by Christian Fermüller and Andrei Voronkov. LNCS 6397, Springer, 2010, pp. 67–81. isbn: 978-3-642-16241-1
  Roland Axelsson, Matthew Hague, Stephan Kreutzer, Martin Lange, and Markus Latte
  (Siehe online unter https://doi.org/10.1007/978-3-642-16242-8_6)
• “GAVS: Game Arena Visualization and Synthesis”. In: 8th International Symposium on Automated Technology for Verification and Analysis (ATVA’10). LNCS 6252, Springer, 2010, pp. 347–352
  C.-H. Cheng, C. Buckl, M. Luttenberger, and A. Knoll
  (Siehe online unter https://doi.org/10.1007/978-3-642-15643-4_26)
• “Generating counterexamples for structural inductions by exploiting nonstandard models”. In: Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17. Ed. by Christian G. Fermüller and Andrei Voronkov. LNCS 6397, Springer, 2010, pp. 117–141
  Jasmin Christian Blanchette and Koen Claessen
  (Siehe online unter https://doi.org/10.1007/978-3-642-16242-8_10)
• “Interprocedural Control Flow Reconstruction”. In: Programming Languages and Systems - 8th Asian Symposium, APLAS 2010. Ed. by Kazunori Ueda. Shanghai, China: LNCS 6461, Springer, 2010, pp. 188–203
  Andrea Flexeder, Bogdan Mihaila, Michael Petter, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-17164-2_14)
• “Local Strategy Improvement for Parity Game Solving”. In: First Symposium on Games, Automata, Logic, and Formal Verification. Vol. 25. EPTCS. 2010, pp. 118–131
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.4204/EPTCS.25.13)
• “Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder”. In: Interactive Theorem Proving, First International Conference, ITP 2010. Ed. by Matt Kaufmann and Lawrence C. Paulson. LNCS 6172, Springer, 2010, pp. 131–146
  Jasmin Christian Blanchette and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-14052-5_11)
• “Non-monotonic Refinement of Control Abstraction for Concurrent Programs”. In: Automated Technology for Verification and Analysis - 8th International Symposium, AT- VA 2010. Ed. by Ahmed Bouajjani and Wei-Ngan Chin. LNCS 6252, Springer, 2010, pp. 188–202
  Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-15643-4_15)
• “On the influence of social factors on team recommendations”. In: Workshops Proceedings of the 26th International Conference on Data Engineering, ICDE 2010. IEEE Computer Society, 2010, pp. 270–277
  Michele Brocco, Georg Groh, and Christian Kern
  (Siehe online unter https://doi.org/10.1109/ICDEW.2010.5452716)
• “The Complexity of Computing Minimal Unidirectional Covering Sets”. In: Algorithms and Complexity, 7th International Conference, CIAC 2010. Ed. by Tiziana Calamoneri and Josep Diaz. LNCS 6078, Springer, 2010, pp. 299–310
  Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, and Jörg Rothe
  (Siehe online unter https://doi.org/10.1007/978-3-642-13073-1_27)
• “The Stevens-Stirling-Algorithm for Solving Parity Games Locally Requires Exponential Time”. In: Int. J. Found. Comput. Sci. 21.3 (2010), pp. 277–287
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.1142/S0129054110007246)
• “Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers”. In: The 8th International Workshop on the Implementation of Logics, IWIL 2010. Ed. by Geoff Sutcliffe, Eugenia Ternovska, and Stephan Schulz. 2010, pp. 1–11
  Lawrence C. Paulson and Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.29007/tnfd)
• “Verifying a Local Generic Solver in Coq”. In: Static Analysis - 17th International Symposium, SAS 2010. LNCS 6337, Springer, 2010, pp. 340–355
  Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-15769-1_21)
• “What Is a Pure Functional?” In: Automata, Languages and Programming, 37th International Colloquium, ICALP 2010. LNCS 6199, Springer, 2010, pp. 199–210
  Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-14162-1_17)
• "Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages”. In: 2nd International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011, Minori, Italy). Ed. by Giovanna D’Agostino and Salvatore La Torre. Vol. 54. EPTCS. 2011, pp. 207– 221
  Markus Latte
  (Siehe online unter https://doi.org/10.4204/EPTCS.54.15)
• “A subexponential lower bound for the Random Facet algorithm for Parity Games”. In: Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SO- DA 2011. 2011, pp. 202–216
  Oliver Friedmann, Thomas Dueholm Hansen, and Uri Zwick
  (Siehe online unter https://doi.org/10.1137/1.9781611973082.19)
• “A Subexponential Lower Bound for Zadeh’s Pivoting Rule for Solving Linear Programs and Games”. In: Integer Programming and Combinatoral Optimization - 15th International Conference, IPCO 2011. 2011, pp. 192–206
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-20807-2_16)
• “Algorithms for synthesizing priorities in componentbased systems”. In: 9th International Symposium on Automated Technology for Verification and Analysis (ATVA’11). LNCS 6996, Springer, 2011, pp. 150–167
  C.-H. Cheng, S. Bensalem, Y.-F. Chen, R-J. Yan, B. Jobstmann, A. Knoll, C. Buckl, and H. Ruess
  (Siehe online unter https://doi.org/10.1007/978-3-642-24372-1_12)
• “An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms”. In: Logical Methods in Computer Science 7.3 (2011)
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.2168/LMCS-7(3:23)2011)
• “Animating the Formalised Semantics of a Java-Like Language”. In: Interactive Theorem Proving - Second International Conference, ITP 2011. Ed. by Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk. LNCS 6898, Springer, 2011, pp. 216–232
  Andreas Lochbihler and Lukas Bulwahn
  (Siehe online unter https://doi. org/10.1007/978-3-642-22863-6_17)
• “Automatic Proof and Disproof in Isabelle/HOL”. In: Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011. Ed. by Cesare Tinelli and Viorica Sofronie-Stokkermans. LNCS 6989, Springer, 2011, pp. 12–27
  Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-24364-6_2)
• “Constraint solving for verification”. PhD thesis. Technical University Munich, 2011
  Ashutosh Gupta
  
• “Exponential Lower Bounds for Solving Infinitary Payoff Games and Linear Programs”. PhD thesis. Ludwig Maximilians University Munich, 2011
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.5282/edoc.13294)
• “Extending H1-clauses with disequalities”. In: Information Processing Letters 111.20 (2011), pp. 1007–1013
  Helmut Seidl and Andreas Reuß
  (Siehe online unter https://doi.org/10.1016/j.ipl.2011.07.011)
• “Extending Hindley- Milner Type Inference with Coercive Structural Subtyping”. In: Programming Languages and Systems - 9th Asian Symposium, APLAS 2011. Ed. by Hongseok Yang. LNCS 7078, Springer, 2011, pp. 89–104
  Dmitriy Traytel, Stefan Berghofer, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-25318-8_10)
• “Extending Sledgehammer with SMT Solvers”. In: Automated Deduction - CADE- 23 - 23rd International Conference on Automated Deduction. Ed. by Nikolaj Bjørner and Viorica Sofronie-Stokkermans. LNCS 6803, Springer, 2011, pp. 207–221
  Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson
  (Siehe online unter https://doi.org/10.1007/978-3-642-22438-6_11)
• “GAVS+: An Open Framework for the Research of Algorithmic Game Solving”. In: TACAS’11. LNCS 6605, Springer, 2011, pp. 258–261
  C.-H. Cheng, A. Knoll, M. Luttenberger, and C. Buckl
  (Siehe online unter https://doi.org/10.1007/978-3-642-19835-9_22)
• “Model Checking Industrial Robot Systems”. In: Model Checking Software - 18th International SPIN Workshop. Ed. by Alex Groce and Madanlal Musuvathi. LNCS 6823, Springer, 2011, pp. 161–176
  Markus Weißmann, Stefan Bedenk, Christian Buckl, and Alois Knoll
  (Siehe online unter https://doi.org/10.1007/978-3-642-22306-8_11)
• “Model Construction and Priority Synthesis for Simple Interaction Systems”. In: 3rd NASA Formal Methods Symposium (NFM’11). LNCS 6617, Springer, 2011, pp. 466–471
  C.-H. Cheng, S. Bensalem, B. Jobstmann, R-J. Yan, A. Knoll, and H. Ruess
  (Siehe online unter https://doi.org/10.1007/978-3-642-20398-5_34)
• “Monotonicity Inference for Higher-Order Formulas”. In: J. Autom. Reasoning 47.4 (2011)
  Jasmin Christian Blanchette and Alexander Krauss
  (Siehe online unter https://doi.org/10.1007/s10817-011-9234-1)
• “More on balanced diets”. In: J. Funct. Program. 21.2 (2011), pp. 135–157
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1017/S0956796810000328)
• “Nitpicking C++ concurrency”. In: 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2011. ACM Press, 2011, pp. 113–124
  Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar
  (Siehe online unter https://doi.org/10.1145/2003476.2003493)
• “On the hardness of priority synthesis”. In: 16th International Conference on Implementation and Application of Automata (CIAA’11). LNCS 6807, Springer, 2011, pp. 110–117
  C.-H. Cheng, B. Jobstmann, C. Buckl, and A. Knoll
  (Siehe online unter https://doi.org/10.1007/978-3-642-22256-6_11)
• “Precise Static Analysis of Binaries by Extracting Relational Information”. In: 18th Working Conference on Reverse Engineering, WCRE 2011. Ed. by M.Pinzger and D. Poshyvanyk. IEEE Computer Society, 2011, pp. 357–366
  A. Sepp, B. Mihaila, and A. Simon
  (Siehe online unter https://doi.org/10.1109/WCRE.2011.50)
• “Predicate abstraction and refinement for verifying multi-threaded programs”. In: 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011. ACM, 2011, pp. 331–344
  Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1145/1926385.1926424)
• “Probabilistic Abstractions with Arbitrary Domains”. In: Static Analysis - 18th International Symposium, SAS 2011. Ed. by Eran Yahav. LNCS 6887, Springer, 2011, pp. 334–350
  Javier Esparza and Andreas Gaiser
  (Siehe online unter https://doi.org/10.1007/978-3-642-23702-7_25)
• “Smart test data generators via logic programming”. In: Technical Communications of the 27th International Conference on Logic Programming, ICLP 2011. Ed. by John P. Gallagher and Michael Gelfond. Vol. 11. LI- PIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011, pp. 139–150
  Lukas Bulwahn
  (Siehe online unter https://doi.org/10.4230/LIPIcs.ICLP.2011.139)
• “Solving Recursion-Free Horn Clauses over LI+UIF”. In: Programming Languages and Systems - 9th Asian Symposium, APLAS 2011. Ed. by Hongseok Yang. LNCS 7978, Springer, 2011, pp. 188–203
  Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-25318-8_16)
• “Subexponential lower bounds for randomized pivoting rules for the simplex algorithm”. In: 43rd ACM Symposium on Theory of Computing, STOC 2011. 2011, pp. 283– 292
  Oliver Friedmann, Thomas Dueholm Hansen, and Uri Zwick
  (Siehe online unter https://doi.org/10.1145/1993636.1993675)
• “Synthesis of Fault-Tolerant Embedded Systems using Games: from Theory to Practice”. In: 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’11). LNCS 6538, Springer, 2011, pp. 118–133
  C.-H. Cheng, H. Ruess, C. Buckl, and A. Knoll
  (Siehe online unter https://doi.org/10.1007/978-3-642-18275-4_10)
• “The Computational Complexity of Weak Saddles”. In: Theory Comput. Syst. 49.1 (2011), pp. 139–161
  Felix Brandt, Markus Brill, Felix A. Fischer, and Jan Hoffmann
  (Siehe online unter https://doi.org/10.1007/s00224-010-9298-z)
• “The Modal µ-Calculus Caught Off Guard”. In: Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011. 2011, pp. 149–163
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-22119-4_13)
• “Threader: A Constraint-Based Verifier for Multi-threaded Programs”. In: Computer Aided Verification - 23rd International Conference, CAV 2011. Ed. by Ganesh Gopalakrishnan and Shaz Qadeer. LNCS 6806, Springer, 2011, pp. 412–417
  Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-22110-1_32)
• “Three Chapters of Measure Theory in Isabelle/HOL”. In: ITP. 2011, pp. 135–151
  Johannes Hölzl and Armin Heller
  (Siehe online unter https://doi.org/10.1007/978-3-642-22863-6_12)
• “Types with potential: polynomial resource bounds via automatic amortized analysis”. PhD thesis. Ludwig Maximilians University Munich, 2011. isbn: 978-3-8442-1516-8
  Jan Hoffmann
  (Siehe online unter https://doi.org/10.5282/edoc.13955)
• "Game solving for industrial automation and control”. In: IE- EE International Conference on Robotics and Automation, ICRA 2012. IEEE Computer Society, 2012, pp. 4367–4372
  Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, and Alois Knoll
  (Siehe online unter https://doi.org/10.1109/ICRA.2012.6224814)
• “Amortised resource analysis for object-oriented programs”. PhD thesis. Ludwig Maximilians University Munich, 2012
  Dulma Rodriguez
  
• “An implementation for algorithmic game solving and its applications in system synthesis”. PhD thesis. Technical University Munich, 2012
  Chih-Hong Cheng
  
• “Automatic proofs and refutations for higherorder logic”. PhD thesis. Technical University Munich, 2012
  Jasmin Christian Blanchette
  
• “Binary Reachability Analysis of Higher Order Functional Programs”. In: Static Analysis - 19th International Symposium, SAS 2012. Ed. by Antoine Miné and David Schmidt. LNCS 7460, Springer, 2012, pp. 388–404
  Ruslán Ledesma-Garza and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-33125-1_26)
• “Branching Time? Pruning Time!” In: Automated Reasoning - 6th International Joint Conference, IJCAR 2012. Ed. by Bernhard Gramlich, Dale Miller, and Uli Sattler. LNCS 7364, Springer, 2012, pp. 393–407
  Markus Latte and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-31365-3_31)
• “Counterexample generation for higher-order logic using functional and logic programming”. PhD thesis. Technical University Munich, 2012
  Lukas Bulwahn
  
• “Crossing the Syntactic Barrier: Hom- Disequalities for H1-Clauses”. In: Implementation and Application of Automata - 17th International Conference, CIAA 2012. Ed. by Nelma Moreira and Rogério Reis. LNCS 7381, Springer, 2012, pp. 301–312
  Andreas Reuß and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-31606-7_26)
• “Distributed priority synthesis using knowledge”. In: 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! 2012. ACM, 2012, pp. 129–132
  Chih-Hong Cheng, Rongjie Yan, Harald Ruess, and Saddek Bensalem
  (Siehe online unter https://doi.acm.org/10.1145/2414639.2414656)
• “Distributed Priority Synthesis”. In: Seventh Conference on Systems Software Verification, SSV 2012. Ed. by Franck Cassez, Ralf Huuck, Gerwin Klein, and Bastian Schlich. Vol. 102. EPTCS. 2012, pp. 57–72
  Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem, and Harald Ruess
  (Siehe online unter https://doi.org/10.4204/EPTCS.102.7)
• “Extending H1-Clauses with Path Disequalities”. In: Foundations of Software Science and Computation Structures - 15th International Conference, FoSSaCS 2012. Ed. by Lars Birkedal. LNCS 7213, Springer, 2012, pp. 165–179
  Andreas Reuß and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-28729-9_11)
• “Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving”. In: 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012. IEEE Computer Society, 2012, pp. 596–605
  Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.1109/LICS.2012.75)
• “Higher-order functional reactive programming in bounded space”. In: 39th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2012. ACM, 2012, pp. 45–58
  Neelakantan R. Krishnaswami, Nick Benton, and Jan Hoffmann
  (Siehe online unter https://doi.org/10.1145/2103621.2103665)
• “HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution)”. In: Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012. LNCS 7214, Springer, 2012, pp. 549–551
  Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-28756-5_46)
• “Improved Single Pass Algorithms for Resolution Proof Reduction”. In: Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012. Ed. by Supratik Chakraborty and Madhavan Mukund. LNCS 7561, Springer, 2012, pp. 107–121
  Ashutosh Gupta
  (Siehe online unter https://doi.org/10.1007/978-3-642-33386-6_10)
• “Interactive verification of Markov chains: Two distributed protocol case studies”. In: Quantities in Formal Methods, QFM 2012. Ed. by Uli Fahrenberg, Axel Legay, and Claus R. Thrane. Vol. 103. EPTCS. 2012, pp. 17–31
  Johannes Hölzl and Tobias Nipkow
  (Siehe online unter https://doi.org/10.4204/EPTCS.103.2)
• “Learn with SAT to Minimize B¨uchi Automata”. In: Third International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2012. Ed. by Marco Faella and Aniello Murano. Vol. 96. EPTCS. 2012, pp. 71–84
  Stephan Barth and Martin Hofmann
  (Siehe online unter https://doi.org/10.4204/EPTCS.96.6)
• “Linear constraints over infinite trees”. In: Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18. LNCS 7180, Springer, 2012, pp. 343–358
  Martin Hofmann and Dulma Rodriguez
  (Siehe online unter https://doi.org/10.1007/978-3-642-28717-6_27)
• “MGSyn: Automatic Synthesis for Industrial Automation”. In: Computer Aided Verification - 24th International Conference, CAV 2012. Ed. by P. Madhusudan and Sanjit A. Seshia. LNCS 7358, Springer, 2012, pp. 658– 664
  Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, and Alois Knoll
  (Siehe online unter https://doi.org/10.1007/978-3-642-31424-7_46)
• “Model Checking Information Flow in Reactive Systems”. In: Verification, Model Checking, and Abstract Interpretation. Ed. by Viktor Kuncak and Andrey Rybalchenko. LNCS 7148, Springer, 2012, pp. 169–185
  Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács Markus Rabe, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-27940-9_12)
• “More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification”. In: Interactive Theorem Proving - Third International Conference, ITP 2012. Ed. by Lennart Beringer and Amy P. Felty. LNCS 7406, Springer, 2012, pp. 345–360
  Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach
  (Siehe online unter https://doi.org/10.1007/978-3-642-32347-8_24)
• “Multivariate amortized resource analysis”. In: ACM Trans. Program. Lang. Syst. 34.3 (2012), 14:1– 14:62
  Jan Hoffmann, Klaus Aehlig, and Martin Hofmann
  (Siehe online unter https://doi.acm.org/10.1145/2362389.2362393)
• “Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL”. In: Interactive Theorem Proving: Third International Conference, ITP 2012. Ed. by Lennart Beringer and Amy Felty. LNCS 7406, Springer, 2012, pp. 377–392. isbn: 978-3-642-32347-8
  Fabian Immler and Johannes Hölzl
  (Siehe online unter https://doi.org/10.1007/978-3-642-32347-8_26)
• “Proving Concurrent Noninterference”. In: Certified Programs and Proofs - Second International Conference, CPP 2012. Ed. by Chris Hawblitzel and Dale Miller. LNCS 7679, Springer, 2012, pp. 109–125
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-35308-6_11)
• “Proving Termination of Probabilistic Programs Using Patterns”. In: Computer Aided Verification - 24th International Conference, CAV 2012. LNCS 7358, Springer, 2012, pp. 123–138
  Javier Esparza, Andreas Gaiser, and Stefan Kiefer
  (Siehe online unter https://doi.org/10.1007/978-3-642-31424-7_14)
• “Rabinizer: Small Deterministic Automata for LTL(F, G)”. In: Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012. LNCS 7561, Springer, 2012, pp. 72–76
  Andreas Gaiser, Jan Křetínský and Javier Esparza
  (Siehe online unter https://doi.org/10.1007/978-3-642-33386-6_7)
• “Ramsey-Based Analysis of Parity Automata”. In: Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012. LNCS 7218, Springer, 2012, pp. 64–78
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-28756-5_6)
• “Reactive and Proactive Diagnosis of Distributed Systems using Net Unfoldings”. In: 12th International Conference on Application of Concurrency to System Design, ACSD 2012. IEEE Computer Society, 2012, pp. 154–163
  Javier Esparza and Christian Kern
  (Siehe online unter https://doi.org/10.1109/ACSD.2012.19)
• “Resource Aware ML”. In: Computer Aided Verification - 24th International Conference, CAV 2012. Ed. by P. Madhusudan and Sanjit A. Seshia. LNCS 7358, Springer, 2012, pp. 781– 786
  Jan Hoffmann, Klaus Aehlig, and Martin Hofmann
  (Siehe online unter https://doi.org/10.1007/978-3-642-31424-7_64)
• “Runtime Enforcement of Information Flow Security in Tree Manipulating Processes”. In: Engineering Secure Software and Systems. Ed. by Gilles Barthe, Benjamin Livshits, and Riccardo Scandariato. LNCS 7159, Springer, 2012, pp. 46–59. isbn: 978-3-642-28165-5
  Máté Kovács and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-642-28166-2_6)
• “Smart testing of functional programs in Isabelle”. In: Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18. Ed. by Nikolaj Bjørner and Andrei Voronkov. LNCS 7180, Springer, 2012, pp. 153–167
  Lukas Bulwahn
  (Siehe online unter https://doi.org/10.1007/978-3-642-28717-6_14)
• “The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof”. In: Certified Programs and Proofs - Second International Conference, CPP 2012. Ed. by Chris Hawblitzel and Dale Miller. LNCS 7679, Springer, 2012, pp. 92–108
  Lukas Bulwahn
  (Siehe online unter https://doi.org/10.1007/978-3-642-35308-6_10)
• “Two Local Strategy Iteration Schemes for Parity Game Solving”. In: Int. J. Found. Comput. Sci. 23.3 (2012), pp. 669– 685
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1142/S0129054112400333)
• “Verifying pCTL Model Checking”. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012). Ed. by C. Flanagan and B. K¨onig. LNCS 7214, Springer, 2012, pp. 347– 361
  Johannes Hölzl and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-28756-5_24)
• “A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions”. In: Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013. LNCS 8123, Springer, 2013, pp. 10–12
  Tobias Nipkow and Maximilian P. L. Haslbeck
  (Siehe online unter https://doi.org/10.1007/978-3-642-40537-2_3)
• “A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars”. In: Inf. Process. Lett. 113.10-11 (2013), pp. 381–385
  Javier Esparza, Andreas Gaiser, and Stefan Kiefer
  (Siehe online unter https://doi.org/10.1016/j.ipl.2013.02.015)
• “A superpolynomial lower bound for strategy iteration based on snare memorization”. In: Discrete Applied Mathematics 161.10-11 (2013), pp. 1317–1337
  Oliver Friedmann
  (Siehe online unter https://doi.org/10.1016/j.dam.2013.02.007)
• “Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis”. In: Computer Aided Verification - 25th International Conference, CAV 2013. Ed. by Natasha Sharygina and Helmut Veith. LNCS 8044, Springer, 2013, pp. 559–575
  Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretínský
  (Siehe online unter https://doi.org/10.1007/978-3-642-39799-8_37)
• “Automatic Type Inference for Amortised Heap-Space Analysis”. In: Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013. Ed. by Matthias Felleisen and Philippa Gardner. LNCS 7792, Springer, 2013, pp. 593–613
  Martin Hofmann and Dulma Rodriguez
  (Siehe online unter https://doi.org/10.1007/978-3-642-37036-6_32)
• “Computing the reveals relation in occurrence nets”. In: Theor. Comput. Sci. 493 (2013), pp. 66–79
  Stefan Haar, Christian Kern, and Stefan Schwoon
  (Siehe online unter https://doi.org/10.1016/j.tcs.2013.04.028)
• “Construction and stochastic applications of measure spaces in higher-order logic”. PhD thesis. Technical University Munich, 2013
  Johannes Hölzl
  
• “Deciding the unguarded modal µcalculus”. In: Journal of Applied Non-Classical Logics 23.4 (2013), pp. 353– 371
  Oliver Friedmann and Martin Lange
  (Siehe online unter https://doi.org/10.1080/11663081.2013.861181)
• “Encoding Monomorphic and Polymorphic Types”. In: Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Ed. by Nir Piterman and Scott A. Smolka. LNCS 7795, Springer, 2013, pp. 493–507
  Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone
  (Siehe online unter https://doi.org/10.1007/978-3-642-36742-7_34)
• “Extending Sledgehammer with SMT Solvers”. In: J. Autom. Reasoning 51.1 (2013), pp. 109–128
  Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson
  (Siehe online unter https://doi.org/10.1007/s10817-013-9278-5)
• “Formal Verification of Language-Based Concurrent Noninterference”. In: J. Formalized Reasoning 6.1 (2013), pp. 1–30
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow
  (Siehe online unter https://dx.doi.org/10.6092/issn.1972-5787/3690)
• “Formalizing Probabilistic Noninterference”. In: Certified Programs and Proofs - Third International Conference, CPP 2013. Ed. by Georges Gonthier and Michael Norrish. LNCS 8307, Springer, 2013, pp. 259–275
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-319-03545-1_17)
• “From tests to proofs”. In: STTT 15.4 (2013), pp. 291–303
  Ashutosh Gupta, Rupak Majumdar, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/s10009-012-0267-5)
• “Information flow security in tree-manipulating processes”. PhD thesis. Technical University Munich, 2013
  Máté Kovács
  
• “JBernstein: A Validity Checker for Generalized Polynomial Constraints”. In: Computer Aided Verification - 25th International Conference, CAV 2013. Ed. by Natasha Sharygina and Helmut Veith. LNCS 8044, Springer, 2013, pp. 656–661
  Chih-Hong Cheng, Harald Ruess, and Natarajan Shankar
  (Siehe online unter https://doi.org/10.1007/978-3-642-39799-8_43)
• “LEO- II and Satallax on the Sledgehammer test bench”. In: J. Applied Logic 11.1 (2013), pp. 91–102
  Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson
  (Siehe online unter https://doi.org/10.1016/j.jal.2012.12.002)
• “MaSh: Machine Learning for Sledgehammer”. In: Interactive Theorem Proving - 4th International Conference, ITP 2013. LNCS 7998, Springer, 2013, pp. 35–50
  Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban
  (Siehe online unter https://doi.org/10.1007/978-3-642-39634-2_6)
• “Mechanizing the Metatheory of Sledgehammer”. In: Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013. Ed. by Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt. LNCS 8152, Springer, 2013
  Jasmin Christian Blanchette and Andrei Popescu
  (Siehe online unter https://doi.org/10.1007/978-3-642-40885-4_17)
• “Methods for the diagnosis and automatic repair of software systems”. PhD thesis. Technical University Munich, 2013
  Christian Kern
  
• “Minimal From Classical Proofs”. In: Annals of Pure and Applied Logic 164.6 (2013), pp. 740–748
  Helmut Schwichtenberg and Christoph Senjak
  (Siehe online unter https://doi.org/10.1016/j.apal.2012.05.009)
• “Monadic Parametricity of Second-Order Functionals”. PhD thesis. Technical University Munich, 2013
  Aleksandr Karbyshev
  
• “MoTraS: A Tool for Modal Transition Systems and Their Extensions”. In: Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Ed. by Dang Van Hung and Mizuhito Ogawa. LNCS 8172, Springer, 2013, pp. 487–491
  Jan Křetínský and Salomon Sickert
  (Siehe online unter https://doi.org/10.1007/978-3-319-02444-8_41)
• “Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference”. In: Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013. Ed. by Reiko Heckel and Stefan Milius. LNCS 8089, Springer, 2013, pp. 236–252
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-642-40206-7_18)
• “Normalization of Horn clauses with disequality constraints”. PhD thesis. Technical University Munich, 2013
  Andreas Reuß
  
• “On Monadic Parametricity of Second-Order Functionals”. In: Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013. Ed. by Frank Pfenning. LNCS 7794, Springer, 2013
  Andrej Bauer, Martin Hofmann, and Aleksandr Karbyshev
  (Siehe online unter https://doi.org/10.1007/978-3-642-37075-5_15)
• “On Refinements of Boolean and Parametric Modal Transition Systems”. In: Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium. Ed. by Zhiming Liu, Jim Woodcock, and Huibiao Zhu. LNCS 8949, Springer, 2013, pp. 213–230
  Křetínský J., Sickert S.
  (Siehe online unter https://doi.org/10.1007/978-3-642-39718-9_13)
• “Rabinizer 2: Small Deterministic Automata for LTL \ GU”. In: Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Ed. by Dang Van Hung and Mizuhito Ogawa. LNCS 8172, Springer, 2013, pp. 446–450
  Křetínský, Jan; Garza, Ruslán Ledesma
  (Siehe online unter https://doi.org/10.1007/978-3-319-02444-8_32)
• “Ramsey Goes Visibly Pushdown”. In: Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Proceedings, Part II. LNCS 7966, Springer, 2013, pp. 224–237
  Oliver Friedmann, Felix Klaedtke, and Martin Lange
  (Siehe online unter https://doi.org/10.1007/978-3-642-39212-2_22)
• “Redirecting Proofs by Contradiction”. In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013. Ed. by Jasmin Christian Blanchette and Josef Urban. Vol. 14. EPiC Series in Computing. EasyChair, 2013, pp. 11–26
  Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.29007/wm8b)
• “Relational abstract interpretation for the verification of 2-hypersafety properties”. In: 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS’13, Berlin. ACM, 2013, pp. 211–222
  Máté Kovács, Helmut Seidl, and Bernd Finkbeiner
  (Siehe online unter https://doi.org/10.1145/2508859.2516721)
• “Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions”. In: Software Quality Journal 21.1 (2013), pp. 101–126
  Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.1007/s11219-011-9148-5)
• “Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs”. In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013. Vol. 14. EPiC Series in Computing. EasyChair, 2013, pp. 117–132
  Steffen Juilf Smolka and Jasmin Christian Blanchette
  (Siehe online unter https://doi.org/10.29007/zbdb)
• “Satisfiability Games for Branching-Time Logics”. In: Logical Methods in Computer Science 9.4 (2013)
  Oliver Friedmann, Markus Latte, and Martin Lange
  (Siehe online unter https://doi.org/10.2168/LMCS-9(4:5)2013)
• “Solving Existentially Quantified Horn Clauses”. In: Computer Aided Verification - 25th International Conference, CAV 2013. LNCS 8044, Springer, 2013, pp. 869–882
  Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.1007/978-3-642-39799-8_61)
• “Solving Parity Games on the GPU”. In: Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. LNCS 8172, Springer, 2013, pp. 455–459
  Philipp Hoffmann and Michael Luttenberger
  (Siehe online unter https://doi.org/10.1007/978-3-319-02444-8_34)
• “Synthesizing Controllers for Automation Tasks with Performance Guarantees”. In: Model Checking Software - 20th International Symposium, SPIN 2013. Ed. by Ezio Bartocci and C. R. Ramakrishnan. LNCS 7976, Springer, 2013, pp. 154–159
  Chih-Hong Cheng, Michael Geisinger, and Christian Buckl
  (Siehe online unter https://doi.org/10.1007/978-3-642-39176-7_10)
• “TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism”. In: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction. Ed. by Maria Paola Bonacina. LNCS 7898, Springer, 2013, pp. 414–420
  Jasmin Christian Blanchette and Andrei Paskevich
  (Siehe online unter https://doi.org/10.1007/978-3-642-38574-2_29)
• “The Undefined Domain: Precise Relational Information for Entities That Do Not Exist”. In: Programming Languages and Systems - 11th Asian Symposium, APLAS 2013. Ed. by Chung-chieh Shan. LNCS 8301, Springer, 2013, pp. 74–89
  Holger Siegel, Bogdan Mihaila, and Axel Simon
  (Siehe online unter https://doi.org/10.1007/978-3-319-03542-0_6)
• “Type Classes and Filters for Mathematical Analysis in Isabelle/HOL”. In: Interactive Theorem Proving - 4th International Conference, ITP 2013. Ed. by Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie. LNCS 7998, Springer, 2013, pp. 279– 294
  Johannes Hölzl, Fabian Immler, and Brian Huffman
  (Siehe online unter https://doi.org/10.1007/978-3-642-39634-2_21)
• “Verification of Reachability Properties and Termination for Probabilistic Systems”. PhD thesis. Technical University Munich, 2013
  Andreas Gaiser
  
• “Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions”. In: ACM SIGPLAN International Conference on Functional Programming, ICFP’13. Ed. by Greg Morrisett and Tarmo Uustalu. ACM, 2013, pp. 3–12
  Dmitriy Traytel and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1145/2544174.2500612)
• “Widening as Abstract Domain”. In: NASA Formal Methods, 5th International Symposium, NFM 2013. LNCS 7871, Springer, 2013, pp. 170–184
  Bogdan Mihaila, Alexander Sepp, and Axel Simon
  (Siehe online unter https://doi.org/10.1007/978-3-642-38088-4_1)
• “A constraint-based approach to solving games on infinite graphs”. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, 2014, pp. 221–234
  Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.acm.org/10.1145/2535838.2535860)
• “An SMT-Based Approach to Coverability Analysis”. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Ed. by Armin Biere and Roderick Bloem. LNCS 8559, Springer, 2014, pp. 603–619
  Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic
  (Siehe online unter https://doi.org/10.1007/978-3-319-08867-9_40)
• “Automatically Generated Safety Mechanisms from Semi-Formal Software Safety Requirements”. In: Computer Safety, Reliability, and Security - 33rd International Conference, SAFECOMP 2014. LNCS 8666, Springer, 2014, pp. 278– 293
  Raphael Fonte Boa Trindade, Lukas Bulwahn, and Christoph Ainhauser
  (Siehe online unter https://doi.org/10.1007/978-3-319-10506-2_19)
• “Branching-time logics with path relativisation”. In: J. Comput. Syst. Sci. 80.2 (2014), pp. 375–389
  Markus Latte and Martin Lange
  (Siehe online unter https://doi.org/10.1016/j.jcss.2013.05.005)
• “Cardinals in Isabelle/HOL”. In: Interactive Theorem Proving - 5th International Conference, ITP 2014. Ed. by Gerwin Klein and Ruben Gamboa. LNCS 8558, Springer, 2014, pp. 111–127
  Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-08970-6_8)
• “CTL+FO verification as constraint solving”. In: 2014 International Symposium on Model Checking of Software, SPIN. ACM, 2014, pp. 101–104
  Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko
  (Siehe online unter https://doi.acm.org/10.1145/2632362.2632364)
• “Experience Report: The Next 1100 Haskell Programmers”. In: Haskell 2014. Ed. by Wouter Swiestra. ACM, 2014, pp. 25–30
  Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1145/2633357.2633359)
• “Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations”. In: NASA Formal Methods: 6th International Symposium, NFM 2014. Ed. by Julia M. Badger and Kristin Yvonne Rozier. LNCS 8430, Springer, 2014, pp. 113–127. isbn: 978-3-319-06200-6
  Fabian Immler
  (Siehe online unter https://doi.org/10.1007/978-3-319-06200-6_9)
• “Generalised Interpolation by Solving Recursion-Free Horn Clauses”. In: First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014. Ed. by Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko, and Valerio Senni. Vol. 169. EPTCS. 2014, pp. 31–38
  Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.4204/EPTCS.169.5)
• “Interprocedural Information Flow Analysis of XML Processors”. In: Language and Automata Theory and Applications - 8th International Conference, LATA 2014. Ed. by Adrian-Horia Dediu, Carlos Martín-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe. LNCS 8370, Springer, 2014, pp. 34–61
  Helmut Seidl and Máté Kovács
  (Siehe online unter https://doi.org/10.1007/978-3-319-04921-2_4)
• “Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata”. In: Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Ed. by Franck Cassez and Jean-François Raskin. LNCS 8837, Springer, 2014, pp. 235– 241
  Komárková, Zuzana; Křetínský, Jan
  (Siehe online unter https://doi.org/10.1007/978-3-319-11936-6_17)
• “Recursive Functions on Lazy Lists via Domains and Topologies”. In: Interactive Theorem Proving - 5th International Conference, ITP 2014. LNCS 8558, Springer, 2014, pp. 341–357
  Andreas Lochbihler and Johannes Hölzl
  (Siehe online unter https://doi.org/10.1007/978-3-319-08970-6_22)
• “Summary-Based Inter-Procedural Analysis via Modular Trace Refinement”. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. Ed. by Venkatesh Raman and S. P. Suresh. Vol. 29. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014, pp. 545– 556
  Franck Cassez, Christian Müller and Karla Burnett
  (Siehe online unter https://doi.org/10.4230/LIPIcs.FSTTCS.2014.545)
• “Synthesizing Predicates from Abstract Domain Losses”. In: NASA Formal Methods - 6th International Symposium, NFM 2014. LNCS 840, Springer, 2014, pp. 328–342
  Bogdan Mihaila and Axel Simon
  (Siehe online unter https://doi.org/10.1007/978-3-319-06200-6_28)
• “Truly Modular (Co)datatypes for Isabelle/HOL”. In: Interactive Theorem Proving - 5th International Conference, ITP 2014. Ed. by Gerwin Klein and Ruben Gamboa. LNCS 8558, Springer, 2014, pp. 93–110
  Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-08970-6_7)
• “Unified Classical Logic Completeness—A Coinductive Pearl”. In: Automated Reasoning - 7th International Joint Conference, IJCAR 2014. Ed. by Stéphane Demri, Deepak Kapur, and Christoph Weidenbach. LNCS 8562, Springer, 2014, pp. 46–60
  Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-08587-6_4)
• “Unified Decision Procedures for Regular Expression Equivalence”. In: Interactive Theorem Proving - 5th International Conference, ITP 2014. Ed. by Gerwin Klein and Ruben Gamboa. LNCS 8558, Springer, 2014, pp. 450–466
  Tobias Nipkow and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-08970-6_29)
• “VeriCon: towards verifying controller programs in software-defined networks”. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014. ACM, 2014, pp. 282–293
  Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, and Asaf Valadarsky
  (Siehe online unter https://doi.org/10.1145/2666356.2594317)
• “A Coalgebraic Decision Procedure for WS1S”. In: 24th EACSL Annual Conference on Computer Science Logic, CSL 2015. Ed. by Stephan Kreutzer. Vol. 41. LIPIcs. Schloss Dagstuhl—Leibniz-Zentrum fA˜14r Informatik, 2015, pp. 487–503
  Dmitriy Traytel
  (Siehe online unter https://doi.org/10.4230/LIPIcs.CSL.2015.487)
• “A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL”. In: Conference on Certified Programs and Proofs. ACM, 2015, pp. 75–83. isbn: 978-1-4503-3296-5
  Manuel Eberl
  (Siehe online unter https://doi.org/10.1145/2676724.2693166)
• “A Formalized Hierarchy of Probabilistic System Types - Proof Pearl”. In: Interactive Theorem Proving - 6th International Conference, ITP 2015. Ed. by Christian Urban and Xingyuan Zhang. LNCS 9236, Springer, 2015, pp. 203–220
  Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-22102-1_13)
• “A Verified Compiler for Probability Density Functions”. In: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015. Ed. by Jan Vitek. LNCS 9032, Springer, 2015, pp. 80–104
  Manuel Eberl, Johannes Hölzl, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-662-46669-8_4)
• “A Verified Enclosure for the Lorenz Attractor (Rough Diamond)”. In: Interactive Theorem Proving: 6th International Conference, ITP 2015. Ed. by Christian Urban and Xingyuan Zhang. LNCS 9236, Springer, 2015, pp. 221–226. isbn: 978-3-319-22102-1
  Fabian Immler
  (Siehe online unter https://doi.org/10.1007/978-3-319-22102-1_14)
• “Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities”. PhD thesis. Technical University Munich, 2015
  Bogdan Mihaila
  
• “An Analysis of Universal Information Flow Based on Self-Composition”. In: IEEE 28th Computer Security Foundations Symposium, CSF 2015. IEEE Computer Society, 2015, pp. 380–393
  Christian Müller, Máté Kovács, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1109/CSF.2015.33)
• “Determining the Nonexistence of Evasive Trajectories for Collision Avoidance Systems”. In: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015. IEEE Computer Society, 2015, pp. 956–961
  Sebastian Söntges and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/ITSC.2015.160)
• “Formalising Traffic Rules for Accountability of Autonomous Vehicles”. In: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015. IEEE Computer Society, 2015, pp. 1658– 1665
  A. Rizaldi and M. Althoff
  (Siehe online unter https://doi.org/10.1109/ITSC.2015.269)
• “Formalizing Symbolic Decision Procedures for Regular Languages”. PhD thesis. Technical University Munich, 2015
  Dmytro Traytel
  
• “Foundational Extensible Corecursion”. In: 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015. Ed. by John Reppy. ACM, 2015, pp. 192–204
  Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1145/2784731.2784732)
• “Interprocedural Two-Variable Herbrand Equalities”. In: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015. Ed. by Jan Vitek. LNCS 9032, Springer, 2015, pp. 457–482
  Stefan Schulze Frielinghaus, Michael Petter, and Helmut Seidl
  (Siehe online unter https://doi.org/10.1007/978-3-662-46669-8_19)
• “Mining the Archive of Formal Proofs”. In: Intelligent Computer Mathematics - International Conference, CICM 2015. Ed. by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge. LNCS 9150, Springer, 2015, pp. 3–17
  Jasmin Christian Blanchette, Maximilian P. L. Haslbeck, Daniel Matichuk, and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-319-20615-8_1)
• “Negotiation Games”. In: Sixth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2015. Vol. 193. EPTCS. 2015, pp. 31–42
  Philipp Hoffmann
  (Siehe online unter https://doi.org/10.4204/EPTCS.193.3)
• “On guarded transformation in the modal µ-calculus”. In: Logic Journal of the IGPL 23.2 (2015), pp. 194–216
  Florian Bruse, Oliver Friedmann, and Martin Lange
  (Siehe online unter https://doi.org/10.1093/jigpal/jzu030)
• “On Time-Memory Trade-Off for Collision Detection”. In: 2015 IEEE Intelligent Vehicles Symposium, IV 2015. IEEE Computer Society, 2015, pp. 1173–1180
  A. Rizaldi, S. S¨ontges, and M. Althoff
  (Siehe online unter https://doi.org/10.1109/IVS.2015.7225842)
• “Ramsey-Based Inclusion Checking for Visibly Pushdown Automata”. In: ACM Trans. Comput. Log. 16.4 (2015), 34:1–34:24
  Oliver Friedmann, Felix Klaedtke, and Martin Lange
  (Siehe online unter https://doi.org/10.1145/2774221)
• “Recursive Games for Compositional Program Synthesis”. In: Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, Revised Selected Papers. Ed. by Arie Gurfinkel and Sanjit A. Seshia. LNCS 9593, Springer, 2015, pp. 19–39
  Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.
  (Siehe online unter https://doi.org/10.1007/978-3-319-29613-5_2)
• “Refinement checking on parametric modal transition systems”. In: Acta Inf. 52.2-3 (2015), pp. 269–297
  Nikola Benes, Jan Křetínský,, Kim G. Larsen, Mikael H. Møller, Salomon Sickert, and Jiří Srba
  (Siehe online unter https://doi.org/10.1007/s00236-015-0215-4)
• “Temporal Program Verification and Synthesis as Horn Constraints Solving”. PhD thesis. Technical University Munich, Germany, 2015
  Tewodros A. Beyene
  
• “Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems”. In: ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. Ed. by Goran Frehse and Matthias Althoff. Vol. 34. EPiC Series in Computing. EasyChair, 2015, pp. 180–187
  Fabian Immler
  (Siehe online unter https://doi.org/10.29007/b3wr)
• “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes”. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015. IEEE Computer Society, 2015, pp. 244–256
  Krishnendu Chatterjee, Zuzana Komárková, and Jan Křetínský
  (Siehe online unter https://doi.org/10.1109/LICS.2015.32)
• “Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions”. In: J. Funct. Program. 25 (2015)
  Dmitriy Traytel and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1017/S0956796815000246)
• “Verified Reachability Analysis of Continuous Systems”. In: Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015. Ed. by Christel Baier and Cesare Tinelli. Berlin, Heidelberg: LNCS 9035, Springer, 2015, pp. 37–51. isbn: 978-3-662- 46681-0
  Fabian Immler
  (Siehe online unter https://doi.org/10.1007/978-3-662-46681-0_3)
• “Witnessing (Co)datatypes”. In: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015. Ed. by Jan Vitek. LNCS 9032, Springer, 2015, pp. 359–382
  Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-662-46669-8_15)
• The Flow of ODEs”. In: Interactive Theorem Proving: 7th International Conference, ITP 2016. Ed. by Jasmin Christian Blanchette and Stephan Merz. LNCS 9807, Springer, 2016, pp. 184– 199. isbn: 978-3-319-43144-4
  Fabian Immler and Christoph Traut
  (Siehe online unter https://doi.org/10.1007/978-3-319-43144-4_12)
• “A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles”. In: NA- SA Formal Methods - 8th International Symposium, NFM 2016. Ed. by Sanjai Rayadurgam and Oksana Tkachuk. LNCS 9690, Springer, 2016, pp. 175–190. isbn: 978-3-319-40648-0
  Albert Rizaldi, Fabian Immler, and Matthias Althoff
  (Siehe online unter https://doi.org/10.1007/978-3-319-40648-0_14)
• “An implementation of Deflate in Coq”. In: FM 2016: Formal Methods - 21st International Symposium. LNCS 9995, Springer, 2016, pp. 612–627
  Christoph-Simon Senjak and Martin Hofmann
  (Siehe online unter https://doi.org/10.1007/978-3-319-48989-6_37)
• “Deciding Monadic Second Order Logic over ω-Words by Specialized Finite Automata”. In: Integrated Formal Methods - 12th International Conference, IFM 2016. Ed. by Eriká Abrahám and Marieke Huisman. LNCS 9681, Springer, 2016, pp. 245–259
  Stephan Barth
  (Siehe online unter https://doi.org/10.1007/978-3-319-33693-0_16)
• “Enforcing Termination of Interprocedural Analysis”. In: Static Analysis - 23rd International Symposium, SAS 2016. Ed. by Xavier Rival. LNCS 9837, Springer, 2016, pp. 447–468
  Stefan Schulze Frielinghaus, Helmut Seidl, and Ralf Vogler
  (Siehe online unter https://doi.org/10.1007/978-3-662-53413-7_22)
• “Efficient CTL Verification via Horn Constraints Solving”. In: 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, 3rd April 2016. Ed. by John P. Gallagher and Philipp Rümmer. Vol. 219. EPTCS. 2016, pp. 1– 14
  Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko
  (Siehe online unter https://doi.org/10.4204/EPTCS.219.1)
• “Fail-Safe Motion Planning of Autonomous Vehicles”. In: 19th IEEE International Conference on Intelligent Transportation Systems, ITSC 2016. IEEE Computer Society, 2016, pp. 452–458
  Silvia Magdici and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/ITSC.2016.7795594)
• “Formal Languages, Formally and Coinductively”. In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Ed. by Delia Kesner and Brigitte Pientka. Vol. 52. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, 31:1–31:17
  Dmitriy Traytel
  (Siehe online unter https://doi.org/10.23638/LMCS-13(3:28)2017)
• “Formalising Semantics for Expected Running Time of Probabilistic Programs”. In: Interactive Theorem Proving - 7th International Conference, ITP 2016. Ed. by Jasmin Christian Blanchette and Stephan Merz. LNCS 9807, Springer, 2016, pp. 475–482
  Johannes Hölzl
  (Siehe online unter https://doi.org/10.1007/978-3-319-43144-4_30)
• “From LTL to deterministic automata - A safraless compositional approach”. In: Formal Methods in System Design 49.3 (2016), pp. 219–271
  Javier Esparza, Jan Křetínský, and Salomon Sickert
  (Siehe online unter https://doi.org/10.1007/s10703-016-0259-2)
• “Limit- Deterministic Büchi Automata for Linear Temporal Logic”. In: Computer Aided Verification - 28th International Conference, CAV 2016. Ed. by Swarat Chaudhuri and Azadeh Farzan. LNCS 9780, Springer, 2016, pp. 312–332
  Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínský
  (Siehe online unter https://doi.org/10.1007/978-3-319-41540-6_17)
• “MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata”. In: Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Ed. by Cyrille Artho, Axel Legay, and Doron Peled. LNCS 9938, Springer, 2016, pp. 130–137
  Salomon Sickert and Jan Křetínský
  (Siehe online unter https://doi.org/10.1007/978-3-319-46520-3_9)
• “Reduction Rules for Colored Workflow Nets”. In: Fundamental Approaches to Software Engineering - 19th International Conference, FASE 2016. LNCS 9633, Springer, 2016, pp. 342–358
  Javier Esparza and Philipp Hoffmann
  (Siehe online unter https://doi.org/10.1007/978-3-662-49665-7_20)
• “Set-Based Prediction of Traffic Participants on Arbitrary Road Networks”. In: IEEE Transactions on Intelligent Vehicles 1.2 (2016), pp. 187–202
  Matthias Althoff and Silvia Magdici
  (Siehe online unter https://doi.org/10.1109/TIV.2016.2622920)
• “Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents”. In: Automated Technology for Verification and Analysis - 14th International Symposium, AT- VA 2016. Ed. by Cyrille Artho, Axel Legay, and Doron Peled. LNCS 9938, Springer, 2016, pp. 157–173
  Bernd Finkbeiner, Helmut Seidl, and Christian Müller
  (Siehe online unter https://doi.org/10.1007/978-3-319-46520-3_11)
• “Verified Analysis of List Update Algorithms”. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. Ed. by Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen. Vol. 65. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, 49:1–49:15
  Maximilian P. L. Haslbeck and Tobias Nipkow
  (Siehe online unter https://doi.org/10.4230/LIPIcs.FSTTCS.2016.49)
• "A Formally Verified Proof of the Central Limit Theorem. In: J Autom Reasoning 59, 389–423 (2017)
  Jeremy Avigad, Johannes Hölzl, and Luke Serafin
  (Siehe online unter https://doi.org/10.1007/s10817-017-9404-x)
• "An exponential lower bound for Cunningham’s rule”. In: Math. Program. 161.1-2 (2017), pp. 271–305
  David Avis and Oliver Friedmann
  (Siehe online unter https://doi.org/10.1007/s10107-016-1008-4)
• “A Report of ARCADE 2017”. In: ARCA- DE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements. Vol. 51. EPiC Series in Computing. EasyChair, 2017, pp. 1–5
  Giles Reger and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.29007/143m)
• “Adaptive Cruise Control with Safety Guarantees for Autonomous Vehicles”. In: World Congress of the International Federation of Automatic Control. IEEE Computer Society, 2017, pp. 5774– 5781
  Silvia Magdici and Matthias Althoff
  (Siehe online unter https://doi.org/10.1016/j.ifacol.2017.08.418)
• “AERIAL: Almost Event- Rate Independent Algorithms for Monitoring Metric Regular Properties”. In: RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools. Ed. by Giles Reger and Klaus Havelund. Vol. 3. Kalpa Publications in Computing. EasyChair, 2017, pp. 29–36
  David A. Basin, Srdjan Krstic, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.29007/bm4c)
• “Almost Event-Rate Independent Monitoring of Metric Dynamic Logic”. In: Runtime Verification - 17th International Conference, RV 2017. Ed. by Shuvendu K. Lahiri and Giles Reger. LNCS 10548, Springer, 2017, pp. 85–102
  David A. Basin, Srdan Krstic, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-67531-2_6)
• “Almost Event-Rate Independent Monitoring of Metric Temporal Logic”. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017. Ed. by Axel Legay and Tiziana Margaria. LNCS 10206, Springer, 2017, pp. 94–112
  David A. Basin, Bhargav Nagaraja Bhatt, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-662-54580-5_6)
• “ARCH-COMP17 Category Report: Continuous Systems with Nonlinear Dynamics”. In: ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek). Ed. by Goran Frehse and Matthias Althoff. Vol. 48. EPiC Series in Computing. EasyChair, 2017, pp. 160–169
  Xin Chen, Matthias Althoff, and Fabian Immler
  (Siehe online unter https://doi.org/10.29007/v6g4)
• “Computing possible driving corridors for automated vehicles”. In: IEEE Intelligent Vehicles Symposium, IV 2017. IEEE Computer Sopciety, 2017, pp. 160–166
  Sebastian Söntges and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/IVS.2017.7995714)
• “Decidable linear list constraints”. In: LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Ed. by Thomas Eiter and David Sands. Vol. 46. EPiC Series in Computing. EasyChair, 2017, pp. 181–199
  Sabine Bauer and Martin Hofmann
  (Siehe online unter https://doi.org/10.29007/d7t4)
• “Determining the maximum time horizon for vehicles to safely follow a trajectory”. In: 20th IEEE International Conference on Intelligent Transportation Systems, ITSC 2017. IEEE Computer Society, 2017, pp. 1–7
  Silvia Magdici, Zhenzhang Ye, and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/ITSC.2017.8317696)
• “Enforcing Termination of Interprocedural Analysis”. In: Formal Methods in System Design (2017)
  Stefan Schulze Frielinghaus, Helmut Seidl, and Ralf Vogler
  (Siehe online unter https://doi.org/10.1007/s10703-017-0288-5)
• “Formal Languages, Formally and Coinductively”. In: Logical Methods in Computer Science 13.3 (2017)
  Dmitriy Traytel
  (Siehe online unter https://doi.org/10.23638/LMCS-13(3:28)2017)
• “Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL”. In: Integrated Formal Methods - 13th International Conference, IFM 2017. Ed. by Nadia Polikarpova and Steve Schneider. LNCS 10510, Springer, 2017, pp. 50– 66
  Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle
  (Siehe online unter https://doi.org/10.1007/978-3-319-66845-1_4)
• “Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic”. In: Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017. Ed. by Clare Dixon and Marcelo Finger. LNCS 10483, Springer, 2017, pp. 3–21
  Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-319-66167-4_1)
• “Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants”. In: Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017. Ed. by Hongseok Yang. LNCS 10201, Springer, 2017, pp. 111–140
  Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/978-3-662-54434-1_5)
• “From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata”. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017. Ed. by Axel Legay and Tiziana Margaria. LNCS 10205, Springer, 2017, pp. 426–442
  Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert
  (Siehe online unter https://doi.org/10.1007/978-3-662-54577-5_25)
• “Interprocedural Two-Variable Herbrand Equalities”. In: Logical Methods in Computer Science 13.2 (2017)
  Stefan Schulze Frielinghaus, Michael Petter, and Helmut Seidl
  (Siehe online unter https://doi.org/10.23638/LMCS-13(2:5)2017)
• “LTL to Deterministic Emerson-Lei Automata”. In: Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017. Ed. by Patricia Bouyer, Andrea Orlandini, and Pierluigi San Pietro. Vol. 256. EPTCS. 2017, pp. 180–194
  David Müller and Salomon Sickert
  (Siehe online unter https://doi.org/10.4204/EPTCS.256.13)
• “Markov Chains and Markov Decision Processes in Isabelle/HOL”. In: J. Autom. Reasoning 59.3 (2017), pp. 345–387
  Johannes Hölzl
  (Siehe online unter https://doi.org/10.1007/s10817-016-9401-5)
• “Markov processes in Isabelle/HOL”. In: 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. Ed. by Yves Bertot and Viktor Vafeiadis. ACM, 2017, pp. 100–111
  Johannes Hölzl
  (Siehe online unter https://doi.acm.org/10.1145/3018610.3018628)
• “Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL”. In: 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. Ed. by Dale Miller. Vol. 84. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017, 11:1–11:18
  Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.4230/LIPIcs.FSCD.2017.11)
• “Polynomial analysis algorithms for free choice Probabilistic Workflow Nets”. In: Perform. Eval. 117 (2017), pp. 104–129
  Javier Esparza, Philipp Hoffmann, and Ratul Saha
  (Siehe online unter https://doi.org/10.1016/j.peva.2017.09.006)
• “Proving Divide and Conquer Complexities in Isabelle/HOL”. In: Journal of Automated Reasoning 58.4 (Apr. 2017), pp. 483–508. issn: 1573- 0670
  Manuel Eberl
  (Siehe online unter https://doi.org/10.1007/s10817-016-9378-0)
• “Soundness and Completeness Proofs by Coinductive Methods”. In: J. Autom. Reasoning 58.1 (2017), pp. 149–179
  Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
  (Siehe online unter https://doi.org/10.1007/s10817-016-9391-3)
• “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes”. In: Logical Methods in Computer Science 13.2 (2017)
  Krishnendu Chatterjee, Zuzana Křetínská and Jan Křetínský
  (Siehe online unter https://doi.org/10.23638/LMCS-13(2:15)2017)
• “Verifying Security Policies in Multi-agent Workflows with Loops”. In: ACM SIGSAC Conference on Computer and Communications Security, CCS 2017. ACM, 2017, pp. 633–645
  Bernd Finkbeiner, Christian Müller, Helmut Seidl, and Eugen Zalinescu
  (Siehe online unter https://doi.org/10.1145/3133956.3134080)
• “A Verified ODE Solver and Smale’s 14th Problem”. PhD thesis. Technical University Munich, 2018
  Fabian Immler
  
• “A Verified ODE Solver and the Lorenz Attractor”. In: J. Autom. Reasoning 61.1-4 (2018), pp. 73–111
  Fabian Immler
  (Siehe online unter https://doi.org/10.1007/s10817-017-9448-y)
• “Computing the Drivable Area of Autonomous Road Vehicles in Dynamic Road Scenes”. In: IEEE Trans. Intelligent Transportation Systems 19.6 (2018), pp. 1855–1866
  Sebastian Söntges and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/TITS.2017.2742141)
• “Hoare Logics for Time Bounds – A Study in Meta Theory”. In: Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TA- CAS 2018. Ed. by M. Huisman and D. Beyer. LNCS 10805, Springer, 2018, pp. 155–171
  Maximilian Paul Louis Haslbeck and Tobias Nipkow
  (Siehe online unter https://doi.org/10.1007/978-3-319-89960-2_9)
• “Interprocedural Program Analysis: Herbrand Equalities and Local Solvers”. PhD thesis. Technical University Munich, Germany, 2018
  Stefan Schulze Frielinghaus
  
• “One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata”. In: LICS
  Javier Esparza, Jan Křetínský and Salomon Sickert
  (Siehe online unter https://doi.org/10.1145/3209108.3209161)
• “Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving”. In: Journal of the ACM 65.2 (Jan. 2018), 6:1–6:28. issn: 0004-5411
  Florian Brandl, Felix Brandt, Manuel Eberl, and Christian Geist
  (Siehe online unter https://doi.org/10.1145/3125642)
• “The Flow of ODEs: Formalization of Variational Equation and Poincaré Map”. In: Journal of Automated Reasoning (2018). issn: 1573-0670
  Fabian Immler and Christoph Traut
  (Siehe online unter https://doi.org/10.1007/s10817-018-9449-5)
• “Verified ip Tables Firewall Analysis and Verification”. In: J. Autom. Reasoning 61.1-4 (2018), pp. 191–242
  Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian P. L. Haslbeck, and Georg Carle
  (Siehe online unter https://doi.org/10.1007/s10817-017-9445-1)
• “Worst-case Analysis of the Time-to-react Using Reachable Sets”. In: IEEE Intelligent Vehicles Symposium, (IV) 2018. IEEE Computer Society, 2018
  Sebastian Söntges, Markus Koschi, and Matthias Althoff
  (Siehe online unter https://doi.org/10.1109/IVS.2018.8500709)