From

Institution

Field

Type

Open access only Cited by patents (Lens) Include non-Aachen papers (citing/cited)

Reset

Papers matching “formal proof” 57

Sort: Relevance Cited Newest Oldest Fwci Patents ⇩ CSV

Not finding it? Sign in to also search OpenAlex live.

Formal Specification and Analysis of OpenJDK's BitSet class: Proof files
2023 Zenodo (CERN European Organization for Nuclear Research) dissertation Computer Science Logic, programming, and type systems Open access

Andy S. Tatman

0

citations
Formal Specification and Analysis of OpenJDK's BitSet class: Proof files
2023 Zenodo (CERN European Organization for Nuclear Research) dissertation Computer Science Logic, programming, and type systems Open access

Andy S. Tatman

0

citations
Formal Specification and Analysis of OpenJDK's BitSet class: Proof files
2023 Zenodo (CERN European Organization for Nuclear Research) dissertation Computer Science Logic, programming, and type systems Open access

Andy S. Tatman

0

citations
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
2020 CEUR Workshop Proceedings article Computer Science Logic, programming, and type systems Open access

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks

0

citations
Analysis and formal specification of OpenJDK's BitSet: Proof files
2024 Science of Computer Programming article Computer Science Logic, programming, and type systems

Andy S. Tatman, Hans-Dieter A. Hiep, Stijn de Gouw

0

citations
New Opportunities for the Formal Proof of Computational Real Geometry?
2020 arXiv (Cornell University) preprint Computer Science Polynomial and algebraic computation Open access

James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks

6

citations
Formal software engineering of distributed systems using focus-streams and automata
2025 RWTH Publications (RWTH Aachen) dissertation Computer Science Formal Methods in Verification Open access

Sebastian Stüber

0

citations
Report on the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
2025 ACM SIGLOG News article Computer Science Logic, programming, and type systems

Emma Ahrens, Jan-Christoph Kassing

0

citations
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium
2023 Lecture notes in computer science conference-paper Computer Science Cryptography and Data Security Open access

Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, +3 more

33

citations
Reasoning About Active Objects: A Sound and Complete Assertional Proof Method
2022 Lecture notes in computer science conference-paper Computer Science Logic, programming, and type systems

Frank S. de Boer, Stijn de Gouw

2

citations
Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
2026 RWTH Publications (RWTH Aachen) dissertation Computer Science Logic, programming, and type systems Open access

Jonas Seidel

0

citations
A time to keep and a time to discard: future-proof data publishing
2025 Zenodo (CERN European Organization for Nuclear Research) article Computer Science Research Data Management Practices Open access

Femmy Admiraal, C. Richard

0

citations
A Sequent Calculus
2021 Graduate texts in mathematics book-chapter Computer Science Logic, programming, and type systems

Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas

0

citations
Formally Verifying Proofs for Algebraic Identities of Matrices
2020 Lecture notes in computer science conference-paper Computer Science Polynomial and algebraic computation

Leonard Schmitz, Viktor Levandovskyy

12

citations
Automated Verification of Proofs in the Universal Composability Framework with Markov Decision Processes
2025 Lecture notes in computer science conference-paper Computer Science Formal Methods in Verification

Maxim Jourenko, Marcus Völker

0

citations
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
2021 arXiv (Cornell University) preprint Computer Science Formal Methods in Verification Open access

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer

0

citations
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
2021 International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) conference-paper Computer Science Formal Methods in Verification Open access

Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport

3

citations
Compositional Reasoning for Parametric Probabilistic Automata
2025 DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) article Computer Science Formal Methods in Verification Open access

1

citations
Quantifier Elimination and Craig Interpolation: The Quantitative Way
2025 Lecture notes in computer science conference-paper Computer Science Formal Methods in Verification Open access

Kevin Batz, Joost-Pieter Katoen, Nora Orhan

0

citations
Quantifier Elimination and Craig Interpolation, Quantitatively
2025 arXiv (Cornell University) preprint Computer Science Formal Methods in Verification Open access

Kevin Batz, Joost-Pieter Katoen, Nora Orhan

0

citations
Formalizing the One-Way to Hiding Theorem
2025 ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) conference-paper Computer Science Quantum Information and Cryptography Open access

Dominique Unruh

1

citations
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
2025 Lecture notes in computer science conference-paper Computer Science Formal Methods in Verification Open access

Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken

6

citations
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
2025 arXiv (Cornell University) preprint Computer Science Formal Methods in Verification Open access

Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken

1

citations
Methoden für die automatische Komplexitäts- und Terminierungsanalyse von (probabilistischen) Programmen und ihre Vollständigkeit
2021 RWTH Publications (RWTH Aachen) dissertation Computer Science Logic, programming, and type systems Open access

Marcel Hark

1

citations
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
2025 arXiv (Cornell University) preprint Computer Science Logic, programming, and type systems Open access

Philipp Schröer, Darion Haase, Joost-Pieter Katoen

0

citations