Talks

2017
Erika Abraham. Symbolic Computation Techniques in SMT Solving, Invited talk at the Evening Seminar of the London Mathematical Society and the British Computer Society at London, UK, 2017.
Erika Abraham. SMT Solving for Real Algebra, Invited talk at the International Conference on Mathematics and Informatics (MathInfo'17), Targu Mures/Marosvásárhely, Romania, 2017.
Erika Abraham. SMT Solving for Arithmetic Theories: Theory and Tool Support, Invited tutorial at the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'17) at Timisoara, Romania, 2017.
DownloadErika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis, Invited talk at the Int. Workshop on Formal Methods for Rigorous Systems Engineering of Cyber-Physical Systems (RISE4CPS), Heidelberg, Germany, 2017.
DownloadFrancesco Leofante. Are you doing what I think you are doing? Robust AI via Verification, Monitoring and Repair, Invited talk at PUMA research training group at Chair for Foundations of Software Reliability and Theoretical Computer Science, Technical University of Munich, Germany, 2017.
DownloadFrancesco Leofante. Optimizing the Performance of Robot Fleets in Production Logistics Scenarios Using SMT Solving, ICT Foundations of Digitized Industry, Economy, and Society Workshop at RWTH Aachen University, Aachen, Germany, 2017.
DownloadErika Abraham. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis, Invited talk at the Int. Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'17), Uppsala, Sweden, 2017.
DownloadErika Abraham. Exploiting Symbolic Computation Techniques in SAT-Modulo-Theories Solving, Invited talk at the University of Waterloo at Waterloo, CA, 2017.
DownloadGereon Kremer. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, Talk at the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, 29th July 2017, Kaiserslautern, Germany, 2017.
DownloadJasper Nalbach. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, Talk at the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, 29th July 2017, Kaiserslautern, Germany, 2017.
DownloadFrancesco Leofante. On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories, Talk at 18th IEEE International Conference on Information Reuse and Integration, San Diego, USA, 2017.
2016
DownloadErika Abraham. Symbolic Computation Techniques in Satisfiability Checking, Invited talk at Johannes Kepler University, RISC, Linz, Autria, 2016.
DownloadErika Abraham, Francesco Leofante. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots, Invited talk at the 7th International Symposium on Leveraging Applications of Formal Methods (ISoLA'16), Verification and Validation, Corfu, Greece, 2016.
DownloadErika Abraham. SMT Solving for Non-Linear Arithmetic Theories, Invited talk at RiSE Seminar, IST Austria, Vienna, Austria, 2016.
DownloadErika Abraham. Computation Techniques in SAT-Modulo-Theories Solving, Invited talk at University of Kassel, Kassel, Germany, 2016.
DownloadErika Abraham. The Power of Satisfiability Checking, Invited talk at European Computer Science Summit (ECSS'16), Budapest, Hungary, 2016.
Gereon Kremer. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, Conference Presentation at 18th Int. Workshop on Computer Algebra in Scientific Computing (CASC'16), Bucharest, Romania, 2016.
DownloadErika Abraham. Symbolic Computation Techniques in Satisfiability Checking, Invited talk at 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), Timisoara, Romania, 2016.
DownloadErika Abraham. Satisfiability Checking: Theory and Applications, Invited talk at 14th International Conference on Software Engineering and Formal Methods (SEFM'16), Vienna, Austria, 2016.
2015
Florian Corzilius, Gereon Kremer. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Talk at Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471), 2015.
DownloadErika Abraham. Current Challenges in the Verification of Hybrid Systems, Invited talk at the 5th Int. Workshop on Cyber Physical Systems (CyPhy'15), Amsterdam, The Netherlands, 2015.
Erika Abraham. Modeling and Verification of Hybrid Systems, Invited lecture series at University of Genoa, Genoa, Italy, 2015.
DownloadErika Abraham. Some Thoughts about Formal Methods in Robotics, Invited talk at University of Genoa, Genoa, Italy, 2015.
Florian Corzilius. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Talk at Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT'15), 2015.
DownloadErika Abraham. Building bridges between symbolic computation and satisfiability checking, Invited talk at 2015 ACM on International Symposium on Symbolic and Algebraic Computation (ISSAC'15), Bath, UK, 2015.
DownloadErika Abraham. A Greedy Approach for the Efficient Repair of Stochastic Controller Models, Invited talk at Abstraction and Synthesis of Correct-by-Construction Robotics Software (AbSynth'15), 2015.
Stefan Schupp. A benchmark suite for hybrid systems reachability analysis, Talk at NFM'15, 2015.
DownloadErika Abraham. Model repair for probabilistic controllers, Invited talk at NII Shonan Meeting “Static Analysis Meets Runtime Verification”, Tokyo, Japan, 2015.
Johanna Nellen, Sascha Geulen. Learning-based Control Strategies for Hybrid Electric Vehicles, Talk at AlgoSyn Seminar, Aachen, Germany, 2015.
Xin Chen. Flow* 1.2: More Effective to Play with Hybrid Systems, Talk at 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Seattle, USA, 2015.
2014
DownloadErika Abraham. SMT solving for real arithmetic: What are the challenges?, Invited talk at CDZ Workshop "Computation and Reasoning with Constraints", Beijing, China, 2014.
Xin Chen. Under-approximate Flowpipes for Non-linear Continous Systems, Talk at the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD'14), Lausanne, Switzerland, 2014.
Erika Abraham. Probabilistic Model Checking and Counterexample Generation, Invited talk at IFIP WG2.2 Meeting on "Formal Description of Programming Concepts", Munich, Germany, 2014.
Johanna Nellen. A CEGAR Approach for the Reachability Analysis of PLC-Controlled Chemical Plants, Talk at 2nd IEEE International Workshop on Formal Methods Integration (FMi'14), 2014.
Gereon Kremer. Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories, Talk at 8th Joint Workshop of the German Research Training Groups in Computer Science, 2014.
DownloadErika Abraham. Reachability Analysis of Hybrid Systems, Invited talk at INRIA, Nancy, France, 2014.
DownloadErika Abraham. Probabilistic Modeling and Model Checking. Invited tutorial, Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software models (SFM-14:ESM), Bertinoro, Italy, 2014.
Erika Abraham. Modeling and Analyzing Probabilistic Systems, Invited talk at NVTI Theory Day, Utrecht, The Netherlands, 2014.
Gereon Kremer, Sebastian Junges. Satisfiability Modulo Real Arithmetic - SMT-Solving with CAD and Gröbner Bases, Talk at Joint Workshop of Research Training Groups PUMA and AlgoSyn, 2014.
Xin Chen. Flow*: Reachability Analysis of Non-Linear Hybrid Systems, Invited talk at the Dagstuhl Seminar "Verification of Cyber-Physical Systems", Dagstuhl, Germany, 2014.
Erika Abraham. Formal Methods for Hybrid Systems. Tutorial, Dagstuhl Seminar "Randomized Timed and Hybrid Models for Critical Infrastructures", Dagstuhl, Germany, 2014.
2013
Erika Abraham. Reachability Analysis for Hybrid Systems, Invited talk at Workshop on Computable Analysis and Rigorous Numerics, Maastricht, The Netherlands, 2013.
Erika Abraham. Formal Methods for Hybrid Systems, Invited talk at University of Passau, Passau, Germany, 2013.
Ulrich Loup, Johanna Nellen. Judging Your Colleagues - Tutorial on ScientistsÂ’ Ratings, Talk at AlgoSyn tutorial, 2013.
Johanna Nellen. Counterexample generation for hybrid automata, Talk at 2nd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Queenstown, New Zealand, 2013.
DownloadErika Abraham. Modeling and Analysis of Hybrid Systems, Invited talk at IFIP WG 2.2 meeting 2013, Lisbon, Portugal, 2013.
DownloadErika Abraham. Reachability Analysis for Hybrid Systems, Invited talk at CDZ Workshop on Probabilistic and Hybrid System Verification, Beijing, China, 2013.
Xin Chen. Lyapunov Function Synthesis using Handelman Representations, Talk at the 9th IFAC Symp. on Nonlinear Control Systems, 2013.
Florian Corzilius. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Talk at the 5th International Conference on Algebraic Informatics (CAI'13), 2013.
DownloadErika Abraham. Eine kurze Einführung in Berechenbarkeit und Komplexität, Talk at the Schüleruniversität Informatik, RWTH Aachen University, Aachen, Germany, 2013.
Erika Abraham. Eine kurze Einführung in die Unentscheidbarkeit, Talk at Aachener Informatiktage, RWTH Aachen University, Germany, 2013.
Ulrich Loup. Dijkstras Algorithmus, Talk at Schüleruniversität Informatik, 2013.
Xin Chen. Flow*: An Analyzer for Non-Linear Hybrid Systems, Talk at the 25th Int. Conf. on Computer Aided Verification (CAV'13), 2013.
Erika Abraham. Informatik != Computer, Talk at Ringvorlesung "Was ist Informatik?", RWTH Aachen University, Aachen, Germany, 2013.
Ulrich Loup. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Invited talk at MPI, Saarbrücken, 2013.
Ulrich Loup. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Talk at AlgoSyn seminar, 2013.
DownloadNils Jansen. Symbolic Counterexample Generation for Discrete-time Markov Chains (with Costs), Talk at MEALS Workshop, Buenos Aires, Argentina, 2013.
2012
DownloadNils Jansen. The COMICS Tool - Computing Minimal Counterexamples for DTMCs, Talk at ATVA, 2012.
DownloadNils Jansen. Symbolic Counterexample Generation for Discrete-time Markov Chains, Talk at FACS, 2012.
Erika Abraham. Computing Counterexamples for Discrete-Time Probabilistic Systems, Tutorial at ROCKS Autumn School "Rigorous Dependability Analysis for Stochastic Systems", Vahrn, Italy, 2012.
Ulrich Loup. SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Talk at AlgoSyn seminar, 2012.
Erika Abraham. Hybrid Systems, Invited talk at University of Twente, Enschede, The Netherlands, 2012.
Ulrich Loup. SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox (Tool Presentation), Talk at SAT, Trento, 2012.
Xin Chen. Using Taylor Models in the Reachability Analysis of Non-linear Hybrid Systems, Talk at the 5th Small Workshop on Interval Methods (SWIMÂ’12), 2012.
Johanna Nellen. Verification of Chemical Plant Control, Talk at Gemeinsamer Workshop der Graduiertenkollegs I: GK 1651 SOAMED et al., 2012.
Erika Abraham. Rechnen mit Nullen und Einsen, Talk at Helle Köpfe in der Informatik, RWTH Aachen University, Aachen, Germany, 2012.
Erika Abraham. Eine kurze Einführung in die Unentscheidbarkeit, Talk for students of a Greek high-school at RWTH Aachen University, Aachen, Germany, 2012.
Ulrich Loup, Johanna Nellen. OASys: An Interdisciplinary DFG Project with Roots in AlgoSyn, Talk at AlgoSyn seminar, 2012.
Erika Abraham. Eine kurze Einführung in die Unentscheidbarkeit, Talk at Ringvorlesung "Was ist Informatik?", RWTH Aachen University, Aachen, Germany, 2012.
Erika Abraham. SMT Solving Mechanisms for Non-Linear Real Arithmetic, Invited talk at Albert-Ludwigs-University, Freiburg, Germany, 2012.
Nils Jansen, Matthias Volk. The Comics Tool - Computing Minimal Counterexamples for DTMCs, Talk at ROCKS Meeting, 2012.
DownloadNils Jansen, Matthias Volk. The COMICS Tool - Computing Minimal Counterexamples for DTMCs, Talk at AlgoSyn Seminar, 2012.
Johanna Nellen. Hybrid Sequential Function Charts, Talk at MBMV, 2012.
Xin Chen. Taylor Model Over-approximations for Flowpipe/Guard Intersections, Talk at NSV, 2012.
Nils Jansen. Symbolic Counterexample Generation for Discrete-time Markov Chains, Talk at AlgoSyn Seminar, 2012.
2011
DownloadUlrich Loup, Sebastian Junges. An Update on Real Algebraic Satisfiability-Modulo-Theories Solving, Talk at AlgoSyn workshop, Rolduc, 2011.
Erika Abraham. Some Decidability Results for Hybrid Automata, Talk at the AlgoSyn Worshop, Rolduc, The Netherlands, 2011.
Johanna Nellen. On Collaboratively Conveying Computer Science to Pupils, Talk at KOLI, 2011.
Erika Abraham. The CEBug Project, Talk at the ROCKS project workshop, München, Germany, 2011.
Erika Abraham. Hierarchical Counterexamples for Discrete-Time Markov Chains, Talk at the 9th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'11), 2011.
DownloadNils Jansen. On Computing Minimal Critical Subsystems for DTMCs, Talk at AlgoSyn Seminar, 2011.
Erika Abraham. Informatik != Computer, Talk at the Schüleruniversität Informatik, RWTH Aachen University, Germany, 2011.
DownloadUlrich Loup. An SMT-Compliant Solver for the Existential Fragment of Real Algebra, Talk at AlgoSyn seminar, 2011.
Erika Abraham. Informatik != Computer, Talk at the Ringvorlesung "Was ist Informatik?", RWTH Aachen University, Germany, 2011.
DownloadUlrich Loup. GiNaCRA: A C++ Library for Real Algebraic Computations, Talk at NFM, Pasadena, 2011.
Johanna Nellen, Ulrich Loup, Jan Oliver Ringert, Wolfgang Thomas. Tutorial on Citation Metrics, Talk at AlgoSyn workshop, Dagstuhl, Germany, 2011.
Nils Jansen. Hierarchical Counterexamples for DTMCs, Talk at AlgoSyn Internal Workshop 2011, 2011.
DownloadNils Jansen, Jens Katelaan. Hierarchical Counterexamples for DTMCs, Talk at Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems, ETAPS, Saarbrücken, Germany, 2011.
DownloadUlrich Loup. GiNaCRA: A C++ Library for Real Algebraic Computations, Talk at AlgoSyn seminar, 2011.
Xin Chen. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems, Talk at Eurocast 2011, 2011.
DownloadFlorian Corzilius. Virtual Substitution for SMT Solving, Talk at In 18th Int. Symp. on Fundamentals of Computation Theory (FCT), 2011.
Johanna Nellen. Confluence Analysis and Completion of Graph Grammars, Talk at the AlgoSyn Seminar, RWTH Aachen University, Germany, 2011.
2010
DownloadErika Abraham. Heap-Abstraction for a Multithreaded Object-Oriented Calculus, Invited talk at Workshop on Automata and Logic for Data Manipulating Programs (LIAFA'10), Paris, France, 2010.
Xin Chen. Reachability Analysis of Continuous Systems with Uncertain Constant Dynamics , Talk at AlgoSyn seminar, RWTH Aachen University, Germany, 2010.
DownloadUlrich Loup. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik, Talk at DeLFI, Duisburg, 2010.
Ulrich Loup. Podcast Production as Collaborative Access to Theoretical Computer Science, Talk at AlgoSyn seminar, 2010.
DownloadNils Jansen. DTMC Model Checking by SCC Reduction, Talk at QEST, Williamsburg, USA, 2010.
Erika Abraham. SMT-Solving for the Reals, Invited talk at University of Karlsruhe, Germany, 2010.
Erika Abraham. Informatik != Computer, Talk at Schüleruniversität Informatik, RWTH Aachen University, Germany, 2010.
Erika Abraham. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra, Invited talk at Dagstuhl Seminar "Verification over Discrete-Continuous Boundaries", Dagstuhl, Germany, 2010.
Erika Abraham. SMT-Solving in the Verification and Synthesis of Hybrid Systems, Invited talk at University of Freiburg, Germany, 2010.
Ulrich Loup. Tutorial on Quotations and BibTeX, Talk at Gemeinsamer Workshop der Informatik-Graduiertenkollegs und Forschungskollegs, 2010.
Nils Jansen. DTMC Model Checking by SCC Reduction, Talk at AlgoSyn Seminar, 2010.
Erika Abraham. Informatik != Computer, Talk at Ringvorlesung "Was ist Informatik?" für Oberstufenschüler, RWTH Aachen University, Aachen, Germany, 2010.
Ulrich Loup. Tutorial on Abstract DPLL, Talk at AlgoSyn workshop, Rolduc, 2010.
Ulrich Loup. Tutorial on Decision Procedures for Real Algebra, Talk at AlgoSyn workshop, Rolduc, 2010.
Nils Jansen. SCC-based Markov Chain Abstraction, Talk at ROCKS Meeting, Molenhoek, Netherlands, 2010.
DownloadUlrich Loup. Actuating Symbolically - A Case Study, Talk at AlgoSyn seminar, 2010.
Erika Abraham. Informatik != Computer, Talk at MINT Winter School, RWTH Aachen University, Germany, 2010.
DownloadErika Abraham. On the Minimization of Hybrid Automata, Talk at the Nordic Workshop on Programming Theory (NWPT'10), 2010.
DownloadErika Abraham. Rewriting-Logic-Based Formal Modeling and Analysis of Interacting Hybrid Systems, Talk at the Nordic Workshop on Programming Theory (NWPT'10), 2010.
Florian Corzilius. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra, Talk at SMT 2010, 2010.
Erika Abraham. SMT-Solving in the Verification and Synthesis of Hybrid Systems, Invited talk at Dagstuhl, Germany, 2010.
Erika Abraham. Tutorial on Satisfiability Checking. Tutorial, AlgoSyn meeting, Rolduc, Germany, 2010.
2009
Erika Abraham. The Theory of Hybrid Systems, Talk at Day of Computer Science (Tag der Informatik), RWTH Aachen University, Aachen, Germany, 2009.
Erika Abraham. SMT-Solving for the First-Order Theory of the Reals, Invited talk at Dagstuhl Seminar "Algorithms and Applications for the Next Generation of SAT Solvers", Dagstuhl, Germany, 2009.
DownloadUlrich Loup. Controller Synthesis of Discrete-Continuous Systems using SMT Solving, Talk at Gemeinsamer Workshop der Informatik-Graduiertenkollegs und Forschungskollegs, Dagstuhl, 2009.
Erika Abraham. SAT-Modulo-Theories Solving in the Context of Bounded Model Checking, Invited talk at CWI Amsterdam, Amsterdam, The Netherlands, 2009.
Ulrich Loup. Controller Synthesis of Discrete-Continuous Systems using SMT Solving, Talk at AlgoSyn seminar, 2009.
Erika Abraham. SMT-solving in the Context of Bounded Model Checking, Invited talk at University of Oslo, Oslo, Norway, 2009.
DownloadUlrich Loup. Decision Problems over the Domain of the Real Numbers, Talk at AlgoSyn seminar, 2009.
2008
Nils Jansen. Automaton-definable Tree Relations with Cardinality Constraints, Talk at AG LuA, RWTH Aachen, 2008.
2006
Erika Abraham. Heap-Abstraction for an Object-Oriented Calculus with Thread Classes, Invited talk at Logical Approaches to Computational Barriers (CiE'06), Swansea, Great Britain, 2006.
Erika Abraham. Parallel SAT Solving in Bounded Model Checking, Talk at Parallel and Distributed Methods in Verification (PDMC'06), 2006.
Erika Abraham. Bounded Model Checking with Parametric Data Structures, Talk at the 4th Int. Workshop on Bounded Model Checking (BMC'06), 2006.
2004
Erika Abraham. A Proof System for Exception Handling in Multithreaded Java, Talk at the Christian-Albrechts-University, Kiel, Germany, 2004.
Erika Abraham. Proof System for Exception Handling in Multithreaded Java, Talk at the Kolloquium Programmiersprachen und Grundlagen der Programmierung, 17.–19. March 2004, Freiburg-Munzingen, 2004.
2003
Erika Abraham. Proving Deadlock Freedom for JavaMT, Talk at the MobiJ-meeting Kiel, 3.-10. June 2003, 2003.
Erika Abraham. A Tool-supported Assertional Proof System for Multithreaded Java, Talk at the Workshop on Formal Techniques for Java-like Programs (FTfJP'03), Darmstadt, Germany, 2003.
2002
Erika Abraham. Verification for Java's monitor concept, Invited talk at Int. Symp. on Formal Methods for Components and Objects (FMCO'02), Leiden, The Netherlands, 2002.
Erika Abraham. A Hoare Logic for Monitors in Java, Invited talk at ICASE - NASA LaRC, 2002.
Erika Abraham. Verification for Java's Reentrant Multithreading Concept, Talk at the 5th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS'02), Grenoble, France, 2002.
2001
Erika Abraham. Verification of Hybrid Systems: Formalization and Proof Rules in PVS, Talk at the Seventh IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS 2001), Skövde, Sweden, 2001.
Erika Abraham. Proof Outlines for Threads in Java, Talk at the Kolloquium Programmiersprachen und Grundlagen der Programmierung, Rurberg, Germany, 2001.
Erika Abraham. Verification for Java's Reentrant Multithreading Concept, Talk at Albert-Ludwigs-University, Freiburg, Germany, 2001.