Armin Biere
@arminbiere
- 29 Followers
- 16 Following
- 21 Posts
Mostly hacking SAT solvers these days.
Universität Freiburg#ChristianStreich mit #Universitätsmedaille ausgezeichnet: Im Rahmen des Alumni-Tags der #UniFreiburg am 4. Juli 2025 wurde dem früheren SC-Freiburg-Trainer und Alumnus die Universitätsmedaille der Universität Freiburg verliehen.
Mate SoosThere's gonna be Summer School on Security Testing and Verification in Brussels in July 7-10.
In case you are interested in fuzzing, testing, verification, software analysis, come along!
I'll be giving a talk on formal verification of smart contracts :)
Our department in lovely Freiburg has an opening for a Full Professorship (W3) on Software Engineering (succession of Andreas Podelski) with a more technical and formal focus https://uni-freiburg.de/en/job/00004237/
Cool video https://youtu.be/0_fdjA2R0bQ?si=p-FDOlRDKK0zG14y explaining how Marijn Heule et.al. solved the mathematical "Empty Hexagon Problem" with the help of SAT (our CaDiCaL actually). This result was first presented at TACAS'24 https://link.springer.com/chapter/10.1007/978-3-031-57246-3_5 and then lifted and formally verified in the Lean theorem prover at ITP'24 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35
This missing number shouldn't have been possible to find.
Kissat dominated the main track of the SAT Competition 2024. It won 3 gold medals!
Core techniques: congruence closure (SAT'24) clausal equivalence sweeping (FMCAD'24), bounded variable addition (BVA) and vivification.
Daniel Le BerreThe results of the Pseudo-Boolean Competition 2024 have been presented at the SAT conference 2024
https://www.cril.univ-artois.fr/PB24/slides.pdf
New this year: certified unsat and optimal answers for some solvers, using VeriPB 2.0 format.
HWMCC'24 Call for Benchmarks and Solvers
https://hwmcc.github.io/2024
Three Single Safety Property Tracks
1. Word-level without arrays (BTOR2)
2. Word-level with arrays (BTOR2)
3. Bit-level with mandatory safety certificates (AIGER)
Benchmarks due August 18
Solvers due September 1
https://hwmcc.github.io/2024
Three Single Safety Property Tracks
1. Word-level without arrays (BTOR2)
2. Word-level with arrays (BTOR2)
3. Bit-level with mandatory safety certificates (AIGER)
Benchmarks due August 18
Solvers due September 1
I am very honoured to have received the Herbrand Award https://cadeinc.org/Herbrand-Award at IJCAR'24 in Nancy last week with the quote: In recognition of his outstanding contributions to satisfiability solving, including innovative applications, methods for formula pre- and in-processing and proof generation, and a series of award-winning solvers, with deep impact on model checking and verification.
The most influential https://www.dac.com/About/DAC-Most-Influential-Paper-Award of 61st DAC'24 goes to the seminal DAC'01 paper "Chaff: Engineering an Efficient SAT Solver" by Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, 2001.