While I don’t understand much algebra, I know Isabelle and implemented a checker in Isabelle/HOL. I used the Refinement Framework and Sepref to generated code in Standard ML. The code is mostly functional (except for the hashmap that is synthesized automatically by Sepref – no need to understand and know anything about it!). How does Pastèque work? I started with an abstract calculus that models the rules of the proofs system. …
Pastèque 2 Pastèque 2 is available on the IsaFoL repository and the HTML generation can be seen too. The source code can be found here. Pastèque 1 Pastèque 1 is available with the Isabelle formalization on the Archive of Formal Proofs, where it is maintained and kept up-to-date. The release is also available here.
2024 Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Proofs for Bounded Model Checking. MBMV'24 Preprint @inproceedings{FazekasPollittFleuryBiere-MBMV24, author = {Katalin Fazekas and Florian Pollitt and Mathias Fleury and Armin Biere}, editor = {Wolfgang Kunz} title = {Incremental Proofs for Bounded Model Checking}, booktitle = {27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems (MBMV'24), Kaiserslautern, Germany}, series = {ITG-Fachberichte}, volume = {314}, pages = {133--143}, publisher = {VDE Verlag}, year = {2024}, } Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques Arxiv version of POS 23 https://arxiv. …
This is the detailed story of my Tweet about the used flag. Database Reduction Some background first. CDCL solvers learns clauses. Actually they generate way too many clauses to keep all of them. So you have to remove them. Actually many of them. This happens during so-called reductions. This comes from the theory of CDCL. There are two way to keep completeness: either delay restarts more-and-more or keep more-and-more clauses. But this does not tell you which clauses you have to keep during reductions. …
Artifacts Reviewing I have consistently felt unease about our approach to examining artifacts. Although I have personally reviewed numerous artifacts, I believe that, as a community, we are mistaken in our methods. Weird Errors and Artifact Problems The objective of artifact creation is straightforward: to enable the reproducibility of results by allowing the same code to be run again in the future. This can be achieved by packaging all necessary components in a repository, such as Zenodo, ensuring that everything is self-contained and does not rely on external internet connections. …