Rigorous Systems Engineering |
|
Description |
The RiSE group focuses on mathematically rigorous methods and techniques for developing software and computer systems. Our research interests cover the entire development process, ranging from the specification of system properties, synthesis of software and hardware components, model-based testing and test case generation, automated formal verification techniques such as model checking, as well as the diagnosis, localization, and repair of faults. |
Group members |
|
Publications |
2020
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher. International Journal on Software Tools for Technology Transfer, volume 22, pages 565-581, 2020. [pdf] [doi]
Thread-modular counter abstraction for parameterized program safety
Thomas Pani, Georg Weissenbacher, Florian Zuleger. Formal methods in computer-aided design, pages 67-76, 2020. [pdf] [doi]
Language inclusion for finite prime event structures
Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher. Verification, model checking, and abstract interpretation, pages 314-336, 2020. [doi]
Preface of the special issue on the conference on formal methods in computer-aided design 2017
Daryl Stewart, Georg Weissenbacher. Formal Methods in System Design, volume 56, pages 1, 2020. [doi]
RAT elimination
Adrian Rebola Pardo, Georg Weissenbacher. Logic for programming, artificial intelligence and reasoning, pages 423-448, 2020. [pdf] [doi]
Multi-linear strategy extraction for QBF expansion proofs via local soundness
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger. SAT 2020: Theory and applications of satisfiability testing - SAT 2020, pages 429-446, 2020. [pdf] [doi] 2019
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher. Model checking software, pages 153-171, 2019. [doi]
Mutation testing with hyperproperties
Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher. Proc. Of SEFM 2019: The 17th international conference on software engineering and formal methods, pages 203-221, 2019. [doi]
Model-based, mutation-driven test-case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher. ACM Transactions on Embedded Computing Systems, volume 18, 2019. [doi]
Model-based diagnosis with multiple observations
Alexey Ignatiev, António Morgado, João Marques-Silva, Georg Weissenbacher. International joint conference on artificial intelligence, pages 1108-1115, 2019. [doi] 2018
A theory of satisfiability-preserving proofs in SAT solving
Adrian Rebola Pardo, Martin Suda. International conference on logic for programming, artificial intelligence and reasoning, pages 583-603, 2018. [pdf] [doi]
Randomized testing of distributed systems with probabilistic guarantees
Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher. Proceedings of the ACM on Programming Languages, volume 2, 2018. [pdf] [doi]
Extended resolution simulates DRAT
Benjamin Kiesl, Adrian Rebola Pardo, Marijn Heule. Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 516-531, 2018. [doi]
A separation logic with data: Small models and automation
Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher. Automated reasoning, pages 455-471, 2018. [pdf] [doi]
Rely-guarantee reasoning for automated bound analysis of lock-free algorithms
Thomas Pani, Georg Weissenbacher, Florian Zuleger. Formal methods in computer-aided design, pages 1-9, 2018. [pdf] [doi] 2017
Fuzzing and verifying RAT refutations with deletion information
Walter Forkel, Tobias Philipp, Adrian Rebola Pardo, Elias Werner. Florida artificial intelligence research society conference, pages 190-193, 2017.
Preface of the special issue in memoriam helmut veith
Georg Gottlob, Thomas A. Henzinger, Georg Weissenbacher. Formal Methods in System Design, volume 51, pages 267-269, 2017. [doi]
Model-based, mutation-driven test case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher. Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design, MEMOCODE 2017, vienna, austria, september 29 - october 02, 2017, pages 56-66, 2017. [doi]
Dynamic reductions for model checking concurrent software
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher. Verification, model checking, and abstract interpretation, pages 246-265, 2017. [doi]
Towards a semantics of unsatisfiability proofs with inprocessing
Tobias Philipp, Adrian Rebola Pardo. Logic programming and automated reasoning (LPAR), pages 65-84, 2017. [pdf] 2016
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher. Formal Methods in System Design, volume 49, pages 1-32, 2016. [doi]
DRAT proofs for XOR reasoning
Tobias Philipp, Adrian Rebola Pardo. Logics in artificial intelligence, pages 415-429, 2016. [doi]
Error invariants for concurrent traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies. Formal methods, pages 370-387, 2016. [doi]
Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Matthias Schlaipfer, Georg Weissenbacher. Journal of Automated Reasoning, volume 57, pages 3-36, 2016. [pdf] [doi] 2015
Proving safety with trace automata and bounded model checking
Matt Lewis, Daniel Kroening, Georg Weissenbacher. Formal methods, pages 325-341, 2015. [doi]
Under-approximating loops in c programs for fast counterexample detection
Matt Lewis, Daniel Kroening, Georg Weissenbacher. Formal Methods in System Design, volume 47, pages 75-92, 2015. [doi]
Boolean satisfiability solvers and their applications in model checking
Yakir Vizel, Georg Weissenbacher, Sharad Malik. Proceedings of the IEEE, volume 103, pages 2021-2035, 2015. [pdf] [doi] 2014
Silicon fault diagnosis using sequence interpolation with backbones
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik. ICCAD, pages 348-355, 2014. [pdf]
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher. Runtime verification, pages 162-177, 2014. [doi]
Counterexample to induction-guided abstraction-refinement (CTIGAR)
Johannes Birgmeier, Aaron Bradley, Georg Weissenbacher. CAV, pages 829-846, 2014. [doi]
Reduction of resolution refutations and interpolants via subsumption
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher. Haifa verification conference (HVC), pages 188-203, 2014. [doi]
Incremental bounded software model checking
Henning Günther, Georg Weissenbacher. SPIN, pages 40-47, 2014. [doi] 2013
Under-approximating loops in c programs for fast counterexample detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher. CAV, pages 381-396, 2013. [doi]
Advanced SAT techniques for abstract argumentation
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran. CLIMA, pages 138-154, 2013. [doi] 2012
Coverage-based trace signal selection for fault localisation in post-silicon validation
Zhu Charlie Shucheng, Georg Weissenbacher, Sharad Malik. Haifa verification conference (HVC), pages 132-147, 2012. [doi]
Interpolant strength revisited
Georg Weissenbacher. International conference on theory and applications of satisfiability testing (SAT), pages 312-326, 2012. [pdf] [doi]
Parallel assertions for architectures with weak memory models
Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik. Automated technology for verification and analysis, pages 254-268, 2012. [doi] |