2025
Formally Verified Cloud-Scale Authorization.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the 47th IEEE/ACM International Conference on Software Engineering, 2025
2024
LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling.
Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024
2023
ALASCA: Reasoning in Quantified Linear Arithmetic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023
A Toolkit for Automated Testing of Dafny.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023
2022
Principles of Contract Languages (Dagstuhl Seminar 22451).
Dagstuhl Reports, November, 2022
Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities.
Proceedings of the IEEE Secure Development Conference, 2022
Reuse of Introduced Symbols in Automatic Theorem Provers (short paper).
Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022
Lemmaless Induction in Trace Logic.
Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC.
Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022
The Rapid Software Verification Framework.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022
Getting Saturated with Induction.
Proceedings of the Principles of Systems Design, 2022
To test, or not to test: A proactive approach for deciding complete performance test initiation.
Proceedings of the IEEE International Conference on Big Data, 2022
2021
From parametric trace slicing to rule systems.
Int. J. Softw. Tools Technol. Transf., 2021
A taxonomy for classifying runtime verification tools.
Int. J. Softw. Tools Technol. Transf., 2021
Making Theory Reasoning Simpler.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021
Eliminating Models During Model Elimination.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021
lazyCoP: Lazy Paramodulation Meets Neurally Guided Search.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021
A Multithreaded Vampire with Shared Persistent Grounding.
Proceedings of the Formal Methods in Computer Aided Design, 2021
On Evaluating Theorem Provers.
Proceedings of the Third International Workshop on Automated Reasoning: Challenges, 2021
2020
Analysing the Performance of Python-Based Web Services with the VyPR Framework.
Proceedings of the Runtime Verification - 20th International Conference, 2020
PerfCI: A Toolchain for Automated Performance Testing during Continuous Integration of Python Projects.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020
Pattern Extraction for Behaviours of Multi-Stage Threats via Unsupervised Learning.
Proceedings of the 2020 International Conference on Cyber Situational Awareness, 2020
Directed Graph Networks for Logical Reasoning (Extended Abstract).
Proceedings of the Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020
A Polymorphic Vampire - (Short Paper).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
A Combinator-Based Superposition Calculus for Higher-Order Logic.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
2019
Runtime Verification Past Experiences and Future Projections.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019
First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Int. J. Softw. Tools Technol. Transf., 2019
The SMT Competition 2015-2018.
J. Satisf. Boolean Model. Comput., 2019
Boldly Going Where No Prover Has Gone Before.
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, 2019
VyPR2: A Framework for Runtime Verification of Python Web Services.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019
International Competition on Runtime Verification (CRV).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019
Specification of temporal properties of functions for runtime verification.
Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019
Explaining Violations of Properties in Control-Flow Temporal Logic.
Proceedings of the Runtime Verification - 19th International Conference, 2019
Symmetry Avoidance in MACE-Style Finite Model Finding.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019
A Neurally-Guided, Parallel Theorem Prover.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019
Induction in Saturation-Based Proof Search.
Proceedings of the Automated Deduction - CADE 27, 2019
Old or Heavy? Decaying Gracefully with Age/Weight Shapes.
Proceedings of the Automated Deduction - CADE 27, 2019
Restricted Combinatory Unification.
Proceedings of the Automated Deduction - CADE 27, 2019
2018
Monitoring Events that Carry Data.
Proceedings of the Lectures on Runtime Verification - Introductory and Advanced Topics, 2018
Introduction to Runtime Verification.
Proceedings of the Lectures on Runtime Verification - Introductory and Advanced Topics, 2018
Specification of State and Time Constraints for Runtime Verification of Functions.
CoRR, 2018
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018
COST Action IC1402 Runtime Verification Beyond Monitoring.
Proceedings of the Runtime Verification - 18th International Conference, 2018
A Broader View on Verification: From Static to Runtime and Back (Track Summary).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018
Some Thoughts About FOL-Translations in Vampire.
Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), 2018
Dynamic Strategy Priority: Empower the Strong and Abandon the Weak.
Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), 2018
Set of Support for Higher-Order Reasoning.
Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), 2018
2017
A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462).
Dagstuhl Reports, 2017
A Story of Parametric Trace Slicing, Garbage and Static Analysis.
Proceedings of the Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, 2017
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).
CoRR, 2017
Testing a Saturation-Based Theorem Prover: Experiences and Challenges.
Proceedings of the Tests and Proofs - 11th International Conference, 2017
Instantiation and Pretending to be an SMT Solver with Vampire.
Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017
A Report of RV-CuBES 2017.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017
Set of Support for Theory Reasoning.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017
Proceedings of the ARCADE 2017, 2017
Checkable Proofs for First-Order Theorem Proving.
Proceedings of the ARCADE 2017, 2017
Runtime Verification Logics A Language Design Perspective.
Proceedings of the Models, Algorithms, Logics and Tools, 2017
2016
Finding Finite Models in Multi-sorted First-Order Logic.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016
Third International Competition on Runtime Verification - CRV 2016.
Proceedings of the Runtime Verification - 16th International Conference, 2016
Proceedings of the Runtime Verification - 16th International Conference, 2016
What Is a Trace? A Runtime Verification Perspective.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016
Considering Typestate Verification for Quantified Event Automata.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016
New Techniques in Clausal Form Generation.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016
The vampire and the FOOL.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016
Better Proof Output for Vampire.
Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016
Global Subsumption Revisited (Briefly).
Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016
2015
Automata-based Pattern Mining from Imperfect Traces.
ACM SIGSOFT Softw. Eng. Notes, 2015
MarQ: Monitoring at Runtime with QEA.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015
Specification of Parametric Monitors.
Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, 2015
From First-order Temporal Logic to Parametric Trace Slicing.
Proceedings of the Runtime Verification - 6th International Conference, 2015
Suggesting Edits to Explain Failing Traces.
Proceedings of the Runtime Verification - 6th International Conference, 2015
Second International Competition on Runtime Verification CRV 2015.
Proceedings of the Runtime Verification - 6th International Conference, 2015
Cooperating Proof Attempts.
Proceedings of the Automated Deduction - CADE-25, 2015
Proceedings of the Automated Deduction - CADE-25, 2015
The Uses of SAT Solvers in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2015
2014
Automata based monitoring and mining of execution traces.
PhD thesis, 2014
The Challenges of Evaluating a New Feature in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014
2013
A Tutorial on Runtime Verification.
Proceedings of the Engineering Dependable Software Systems, 2013
A pattern-based approach to parametric specification mining.
Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013
2012
Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors.
Proceedings of the FM 2012: Formal Methods, 2012