Forschungsbereich Formal Methods in Systems Engineering

Organization Name (de) Name der Organisation (de)
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
 
Code Kennzahl
E192-04
 
Type of Organization Organisationstyp
Research Division
Parent OrgUnit Übergeordnete Organisation
 
Active Aktiv
 


Results 1-100 of 502 (Search time: 0.001 seconds).

PreviewAuthors / EditorsTitleTypeIssue Date
1Nießen, Tobias ; Paverd, Andrew Trusted and Transparent Time-Stamping Through TEEs and Network Time SecurityInproceedings Konferenzbeitrag 26-Apr-2026
2Schreiber, Dominik ; Fleury, Mathias ; Fazekas, Katalin ; Biere, Armin Real-time Proof Checking for Distributed Incremental SAT SolvingInproceedings Konferenzbeitrag 16-Apr-2026
3Sextl-2026-Brushing off the Rust Towards Compositional Memory Safety Veri...-vor.pdf.jpgSextl, Florian Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe RustPresentation Vortrag 13-Apr-2026
4King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura LLMs and fuzzing in tandem: a new approach to automatically generating weakest preconditionsArticle Artikel 12-Mar-2026
5El Manssour, Rida Ait ; Kenison, George ; Shirmohammadi, Mahsa ; Varonka, Anton ; Worrell, James B Determination Problems for Orbit Closures and Matrix GroupsInproceedings Konferenzbeitrag 8-Jan-2026
6Rawson, Michael ; Eisenhofer, Clemens ; Kovács, Laura Constraint Learning for Non-confluent Proof SearchInproceedings Konferenzbeitrag 2026
7Eisenhofer, Clemens ; Seiser, Theodor ; Bjørner, Nikolaj ; Kovács, Laura On Solving String Equations via Powers and Parikh ImagesInproceedings Konferenzbeitrag 2026
8Kolluri, Aashish ; Sharma, Rishi ; Costa, Manuel ; Köpf, Boris ; Nießen, Tobias ; Russinovich, Mark ; Tople, Shruti ; Zanella Béguelin, Santiago Optimizing Agent Planning for Security and AutonomyInproceedings Konferenzbeitrag 2026
9Correnson-2025-Acta Informatica-vor.pdf.jpgCorrenson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg Symbolic execution for refuting ∀∃ hyperpropertiesArticle Artikel Dec-2025
10Rain, Sophie ; Petković Komel, Anja ; Rawson, Michael ; Kovacs, Laura Game Modeling of Blockchain ProtocolsInproceedings Konferenzbeitrag 15-Nov-2025
11Hajdu, Márton ; Hozzová, Petra ; Kovacs, Laura ; Voronkov, Andrei ; Wagner, Eva Maria ; Žilinčík, Richard Steven Synthesis Benchmarks for Automated ReasoningInproceedings Konferenzbeitrag 8-Oct-2025
12Winkler, Lorenz ; Kovács, Laura Positive Almost-Sure Termination of Polynomial Random WalksInproceedings Konferenzbeitrag 2-Oct-2025
13Bocevska, Ivana ; Petković Komel, Anja ; Kovacs, Laura ; Rain, Sophie ; Rawson, Michael Divide and Conquer: A Compositional Approach to Game-Theoretic SecurityArticle Artikel Oct-2025
14Bozga, Marius ; Iosif, Radu ; Zuleger, Florian Regular Grammars for Sets of Graphs of Tree-Width 2Inproceedings Konferenzbeitrag Oct-2025
15Hajdu, Marton ; Kovács, Laura ; Voronkov, Andrei Partial Redundancy in SaturationInproceedings Konferenzbeitrag 24-Sep-2025
16Kaufmann, Daniela Verifying Arithmetic Circuits with PolynomialsPresentation Vortrag24-Sep-2025
17Bártek, Filip ; Bhayat, Ahmed ; Coutelier, Robin ; Hajdu, Márton ; Hetzenberger, Matthias ; Hozzová, Petra ; Kovács, Laura ; Rath, Jakob ; Rawson, Michael ; Reger, Giles ; Suda, Martin ; Schoisswohl, Johannes ; Voronkov, Andrei The Vampire DiaryInproceedings Konferenzbeitrag 24-Sep-2025
18Pluska, Alexander ; Malhotra, Sagar On Local Limits of Sparse Random Graphs: Color Convergence and the Refined Configuration ModelInproceedings Konferenzbeitrag 18-Sep-2025
19Varonka, Anton ; Watanabe, Kazuki On Piecewise Affine Reachability with Bellman OperatorsInproceedings Konferenzbeitrag 20-Aug-2025
20Hofstadler, Clemens ; Kaufmann, Daniela Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit VerificationInproceedings Konferenzbeitrag 8-Aug-2025
21Codel-2025-Proceedings of SAT Competition 2025  Solver and Benchmark Desc...-vor.pdf.jpgCodel, Cayden ; Fazekas, Katalin ; Heule, Marijn J. H. ; Iser, Markus Proceedings of SAT Competition 2025 : Solver and Benchmark DescriptionsProceedings Tagungsband Aug-2025
22Hajdu, Marton ; Coutelier, Robin ; Kovacs, Laura ; Voronkov, Andrei Term Ordering DiagramsInproceedings Konferenzbeitrag 30-Jul-2025
23Aminof, Benjamin ; Rubin, Sasha ; Spegni, Francesco ; Zuleger, Florian Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast SystemsArticle Artikel 24-Jun-2025
24King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura LLM-based Generation of Weakest Preconditions and Precise Array InvariantsInproceedings Konferenzbeitrag 12-Jun-2025
25Kovacs-2025-Automated Reasoning-vor.pdf.jpgKovacs, Laura Automated ReasoningPresentation Vortrag Jun-2025
26Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura PolySAT: Word-level Bit-vector Reasoning in Z3Inproceedings Konferenzbeitrag 3-May-2025
27Sextl, Florian ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian Compositional Shape Analysis with Shared Abduction and Biabductive Loop AccelerationInproceedings Konferenzbeitrag 1-May-2025
28Kaufmann, Daniela ; Berthomieu, Jérémy Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter GraphsInproceedings Konferenzbeitrag 1-May-2025
29Sextl, Florian ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)Presentation Vortrag21-Jan-2025
30Moosbrugger, Marcel ; Müllner, Julian ; Bartocci, Ezio ; Kovacs, Laura Polar: An Algebraic Analyzer for (Probabilistic) LoopsBook Contribution Buchbeitrag 2025
31Ait El Manssour, Rida ; Kenison, George ; Shirmohammadi, Mahsa ; Varonka, Anton Simple Linear Loops: Algebraic Invariants and ApplicationsInproceedings Konferenzbeitrag 2025
32Irfan, Ahmed ; Kaufmann, Daniela Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025Proceedings Tagungsband 2025
33Kaufmann, Daniela ; Hofstadler, Clemens Recycling Algebraic Proof CertificatesInproceedings Konferenzbeitrag 2025
34Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin Incremental Inprocessing Rules beyond ResolutionInproceedings Konferenzbeitrag 2025
35Bozga, Marius ; Iosif, Radu ; Zuleger, Florian Iterating Non-Aggregative Structure CompositionsInproceedings Konferenzbeitrag2025
36Simader, Marcel ; Rebola-Pardo, Adrian ; Seidl, Martina FERAT: A New Expansion-Based Certification Framework for Quantified Boolean FormulasInproceedings Konferenzbeitrag 2025
37Fazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin Satisfiability Modulo User PropagatorsArticle Artikel 27-Dec-2024
38Pani, Thomas ; Weissenbacher, Georg ; Zuleger, Florian Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verificationArticle Artikel Dec-2024
39Brechelmacher-2024-Differential Property Monitoring forBackdoor Detection-am.pdf.jpgBrechelmacher, Otto ; Ničković, Dejan ; Nießen, Tobias ; Sallinger, Sarah Sophie ; Weissenbacher, Georg Differential Property Monitoring for Backdoor DetectionInproceedings Konferenzbeitrag 29-Nov-2024
40Loitzl, Alexander ; Zuleger, Florian Modeling Register Pairs in CompCertInproceedings Konferenzbeitrag 13-Nov-2024
41Coutelier-2024-Formal Methods in System Design-vor.pdf.jpgCoutelier, Robin ; Rath, Jakob ; Rawson, Michael ; Biere, Armin ; Kovacs, Laura SAT solving for variants of first-order subsumptionArticle Artikel 11-Nov-2024
42Aminof, Benjamin ; De Giacomo, Guiseppe ; Rubin, Sasha ; Zuleger, Florian Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive SynthesisInproceedings Konferenzbeitrag Nov-2024
43Fazekas, Katalin SAT modulo IPASIR-UPPresentation Vortrag14-Oct-2024
44Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura PolySAT: Word-level Bit-vector Reasoning in Z3Presentation Vortrag14-Oct-2024
45Correnson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg Finding ∀∃ Hyperbugs using Symbolic ExecutionArticle Artikel 8-Oct-2024
46Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils Clausal Equivalence SweepingInproceedings Konferenzbeitrag Oct-2024
47Ait El Manssour, Rida ; Kenison, George James ; Shirmohammadi, Mahsa ; Varonka, Anton Simple Linear Loops: Algebraic Invariants and SynthesisPresentation Vortrag19-Sep-2024
48Sextl, Florian With Biabduction towards Memory Safety across the Rust-C-FFIPresentation Vortrag17-Sep-2024
49Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils Clausal Congruence ClosureInproceedings Konferenzbeitrag 19-Aug-2024
50Coutelier, Robin ; Fleury, Mathias ; Kovacs, Laura Lazy Reimplication in Chronological BacktrackingInproceedings Konferenzbeitrag 19-Aug-2024
51Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin Certifying Incremental SAT SolvingPresentation Vortrag23-Jul-2024
52Kofnov-2024-ACM Transactions on Modeling and Computer Simulation-vor.pdf.jpgKofnov, Andrey ; Moosbrugger, Marcel ; Stankovic, Miroslav ; Bartocci, Ezio ; Bura, Efstathia Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial AssignmentsArticle Artikel 10-Jul-2024
53Hader, Thomas ; Kaufmann, Daniela ; Irfan, Ahmed ; Graham-Lengrand, Stéphane ; Kovács, Laura MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper)Inproceedings Konferenzbeitrag 1-Jul-2024
54Indri, Patrick ; Blohm, Peter ; Athavale, Anagha ; Bartocci, Ezio ; Weissenbacher, Georg ; Maffei, Matteo ; Nickovic, Dejan ; Gärtner, Thomas ; Malhotra, Sagar Distillation based Robustness Verification with PAC GuaranteesInproceedings Konferenzbeitrag 28-Jun-2024
55Fazekas, Katalin Incremental SAT Solvers in PracticePresentation Vortrag26-Jun-2024
56Nastran, Martin ; Peschek, Paul ; Walendzik, Izabela ; Rath, Jakob ; Fickl, Bernhard ; Schubert, Jasmin Sophia ; Szabo, Gabriel ; Wilhelm, Richard Arthur ; Schmidt, Jochen ; Eder, Dominik ; Bayer-Skoff, Bernhard High-yield liquid phase exfoliation of graphene utilizing low boiling co-solvent solutions and ammoniaPresentation Vortrag24-Jun-2024
57Pluska-2024-Logical Distillation of Graph Neural Networks-vor.pdf.jpgPluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar Logical Distillation of Graph Neural NetworksInproceedings Konferenzbeitrag 24-Jun-2024
58Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin Incremental Proofs for Bounded Model CheckingInproceedings Konferenzbeitrag 19-Jun-2024
59Amrollahi, Daneshvar ; Bartocci, Ezio ; Kenison, George James ; Kovacs, Laura ; Moosbrugger, Marcel ; Stankovic, Miroslav (Un)Solvable loop analysisArticle Artikel 11-Jun-2024
60AL-Zubi-2024-Statistical Profiling of Micro-Architectural Traces and Machi...-am.pdf.jpgAL-Zu'bi, Mai ; Weissenbacher, Georg Statistical Profiling of Micro-Architectural Traces and Machine Learning for Spectre Detection: A Systematic EvaluationInproceedings Konferenzbeitrag 10-Jun-2024
61Chimes, Mark Jonathan ; Iosif, Radu ; Zuleger, Florian Tree-Verifiable Graph GrammarsInproceedings Konferenzbeitrag 26-May-2024
62Georgiou-2024-Saturating Sorting without Sorts-vor.pdf.jpgGeorgiou, Pamina ; Hajdu, Marton ; Kovacs, Laura Saturating Sorting without SortsInproceedings Konferenzbeitrag 26-May-2024
63Hajdu-2024-Rewriting and Inductive Reasoning-vor.pdf.jpgHajdu, Marton ; Kovács, Laura ; Rawson, Michael Rewriting and Inductive ReasoningInproceedings Konferenzbeitrag 26-May-2024
64Schoisswohl-2024-VIRAS Conflict-Driven Quantifier Elimination for Integer...-vor.pdf.jpgSchoisswohl, Johannes ; Kovács, Laura ; Korovin, Konstantin VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real ArithmeticInproceedings Konferenzbeitrag 26-May-2024
65Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin Certifying Incremental SAT SolvingInproceedings Konferenzbeitrag 26-May-2024
66Dacík, Tomáš ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian Deciding Boolean Separation Logic via Small ModelsInproceedings Konferenzbeitrag 4-Apr-2024
67Hitarth, S. ; Kenison, George James ; Kovacs, Laura ; Varonka, Anton Linear Loop Synthesis for Quadratic InvariantsInproceedings Konferenzbeitrag 11-Mar-2024
68Georgiou, Pamina ; Hajdu, Márton ; Kovács, Laura Saturating Sorting without SortsPreprint Preprint 6-Mar-2024
69Sochor, Hannes ; Ferrarotti, Flavio ; Kaufmann, Daniela Fuzzing-based grammar learning from a minimal set of seed inputsArticle Artikel Mar-2024
70Niessen-2024-Finding counterexamples to  hyperproperties-am.pdf.jpgNießen, Tobias ; Weissenbacher, Georg Finding counterexamples to ∀∃ hyperpropertiesPresentation Vortrag 16-Jan-2024
71Müllner, Julian ; Moosbrugger, Marcel ; Kovács, Laura Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) ProgramsArticle Artikel 5-Jan-2024
72Eisenhofer-2024-Embedding the Connection Calculus in Satisfiability Modul...-vor.pdf.jpgEisenhofer, Clemens ; Kovács, Laura ; Rawson, Michael Embedding the Connection Calculus in Satisfiability Modulo TheoriesInproceedings Konferenzbeitrag Jan-2024
73Jeanteur, Simon ; Kovács, Laura ; Maffei, Matteo ; Rawson, Michael CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic ModelInproceedings Konferenzbeitrag 2024
74Ciabattoni, Agata ; Eisenhofer, Clemens ; Rozplokhas, Dmitry Strongly Analytic Calculi for KLM Logics with SMT-Based ProverInproceedings Konferenzbeitrag 2024
75Pluska-2024-Logical Distillation of Graph Neural Networks-vor.pdf.jpgPluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar Logical Distillation of Graph Neural NetworksInproceedings Konferenzbeitrag 2024
76Aminof, Benjamin ; Cooper, Linus ; Rubin, Sasha ; Vardi, Moshe Y. ; Zuleger, Florian Probabilistic Synthesis and Verification for LTL on Finite TracesInproceedings Konferenzbeitrag 2024
77Kovacs-2024-Induction inSaturation-vor.pdf.jpgKovács, Laura ; Hozzová, Petra ; Hajdu, Márton ; Voronkov, Andrei Induction in SaturationInproceedings Konferenzbeitrag 2024
78Hozzová, Petra ; Amrollahi, Daneshvar ; Hajdu, Márton ; Kovács, Laura ; Voronkov, Andrei ; Wagner, Eva Maria Synthesis of Recursive Programs in SaturationInproceedings Konferenzbeitrag 2024
79Biere, Armin ; Faller, Tobias ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils ; Pollitt, Florian CaDiCaL 2.0Inproceedings Konferenzbeitrag 2024
80Hajdu-2024-Reducibility Constraints inSuperposition-vor.pdf.jpgHajdu, Márton ; Kovács, Laura ; Rawson, Michael ; Voronkov, Andrei Reducibility Constraints in SuperpositionInproceedings Konferenzbeitrag 2024
81Heisinger-2024-Quantifier Shifting forQuantified Boolean Formulas Revisited-vor.pdf.jpgHeisinger, Simone ; Heisinger, Maximilian ; Rebola-Pardo, Adrian ; Seidl, Martina Quantifier Shifting for Quantified Boolean Formulas RevisitedInproceedings Konferenzbeitrag 2024
82Athavale, Anagha ; Bartocci, Ezio ; Christakis, Maria ; Maffei, Matteo ; Ničković, Dejan ; Weissenbacher, Georg Verifying Global Two-Safety Properties in Neural Networks with ConfidenceInproceedings Konferenzbeitrag 2024
83Rain, Sophie ; Brugger, Lea Salome ; Petković Komel, Anja ; Kovács, Laura ; Rawson, Michael Scaling CheckMate for Game-Theoretic SecurityInproceedings Konferenzbeitrag 2024
84Hader, Thomas ; Ozdemir, Alex An SMT-LIB Theory of Finite FieldsInproceedings Konferenzbeitrag 2024
85Amrollahi, Daneshvar ; Bartocci, Ezio ; Kenison, George ; Kovacs, Laura ; Moosbrugger, Marcel ; Stankovič, Miroslav Correction: (Un)Solvable loop analysisArticle Artikel2024
86Brugger-2023-CheckMate Automated Game-Theoretic Security Reasoning-vor.pdf.jpgBrugger, Lea Salome ; Kovács, Laura ; Petkovic Komel, Anja ; Rain, Sophie ; Rawson, Michael CheckMate: Automated Game-Theoretic Security ReasoningInproceedings Konferenzbeitrag 21-Nov-2023
87Moosbrugger, Marcel ; Müllner, Julian ; Kovács, Laura Automated Sensitivity Analysis for Probabilistic LoopsInproceedings Konferenzbeitrag 6-Nov-2023
88Sallinger-2023-A Formalization ofHeisenbugs andTheir Causes-am.pdf.jpgSallinger, Sarah ; Weissenbacher, Georg ; Zuleger, Florian A Formalization of Heisenbugs and Their CausesInproceedings Konferenzbeitrag 31-Oct-2023
892023-Reshaping Unplugged Computer Science Workshops forPrimary School Edu...-vor.pdf.jpgLandman, Martina ; Rain, Sophie ; Kovács, Laura ; Gerald Futschek Reshaping Unplugged Computer Science Workshops for Primary School EducationInproceedings Konferenzbeitrag 1-Oct-2023
90Fazekas-2023-SAT-Based Quantified Symmetric Minimization of the Reachable...-vor.pdf.jpgFazekas, Katalin ; Aman, Goel ; Sakallah, Karem SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed ProtocolsInproceedings Konferenzbeitrag Oct-2023
91Rozier-2023-Developing an Open-Source, State-of-the-Art Symbolic Model-Ch...-vor.pdf.jpgRozier, Kristin Yvonne ; Shankar, Natarajan ; Tinelli, Cesare ; Vardi, Moshe Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research CommunityInproceedings Konferenzbeitrag Oct-2023
92Andriushchenko, Roman ; Bartocci, Ezio ; Češka, Milan ; Pontiggia, Francesco ; Sallinger, Sarah Sophie Deductive Controller Synthesis for Probabilistic HyperpropertiesInproceedings Konferenzbeitrag 15-Sep-2023
93Rawson, Michael ; Wernhard, Christoph ; Zombori, Zsolt ; Bibel, Wolfgang Lemmas: Generation, Selection, ApplicationInproceedings Konferenzbeitrag 14-Sep-2023
94Eisenhofer-2023-Non-Classical Logics inSatisfiability Modulo Theories-vor.pdf.jpgEisenhofer, Clemens ; Alassaf, Ruba ; Rawson, Michael ; Kovács, Laura Non-Classical Logics in Satisfiability Modulo TheoriesInproceedings Konferenzbeitrag 14-Sep-2023
95Bjørner, Nikolaj ; Fazekas, Katalin On Incremental Pre-processing for SMTInproceedings Konferenzbeitrag 2-Sep-2023
96Coutelier, Robin ; Kovács, Laura ; Rawson, Michael ; Rath, Jakob SAT-Based Subsumption ResolutionInproceedings Konferenzbeitrag2-Sep-2023
97Hozzova-2023-Program Synthesis inSaturation-vor.pdf.jpgHozzová, Petra ; Kovács, Laura ; Norman, Chase ; Voronkov, Andrei Program Synthesis in SaturationInproceedings Konferenzbeitrag 2-Sep-2023
98Bhayat, Ahmed ; Schoisswohl, Johannes ; Rawson, Michael Superposition with Delayed UnificationInproceedings Konferenzbeitrag2-Sep-2023
99Ayala, Pablo ; Naghdi, Shaghayegh ; Nandan, Sreejith P. ; Myakala, Stephen Nagaraju ; Rath, Jakob ; Saito, Hikaru ; Guggenberger, Patrick ; Lakhanlal, Lakhanlal ; Kleitz, Freddy ; Toroker, Maytal Caspary ; Cherevan, Alexey ; Eder, Dominik The Emergence of 2D Building Units in Metal‐Organic Frameworks for Photocatalytic Hydrogen Evolution: A Case Study with COK‐47Article Artikel 18-Aug-2023
100Fazekas-2023-IPASIR-UP User Propagators for CDCL-vor.pdf.jpgFazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin IPASIR-UP: User Propagators for CDCLInproceedings Konferenzbeitrag 9-Aug-2023