Publications
To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.
STSM reports
2025
- Learning Structure-Aware Representations of Dependent Types, Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy, 38th Annual Conference on Neural Information Processing Systems (NeurIPS’24).
- Type-Theory of Algorithms with Chain-Free Memory, Roussanka Loukanova, 21st International Conference on Distributed Computing and Artificial Intelligence (DCAI’24).
2024
- Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDX, Muhammad Usama Sardar, Arto Niemi, Hannes Tschofenig, Thomas Fossati, IEEE Access, pp. 173670-173685, vol 12.
- Semantics of Propositional Attitudes in Type-Theory of Algorithms, Roussanka Loukanova, Logic and Engineering of Natural Language Semantics (LENLS) 2023, LNCS 14569.
- Mechanized HOL Reasoning in Set Theory. Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak. ITP 2024.
- SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus. Julie Cailler, Simon Guilloud. PAAR 2024.
- Orthologic with Axioms. Simon Guilloud, Viktor Kunčak. POPL 2024.
- Interpolation and Quantifiers in Ortholattices. Simon Guilloud, Sankalp Gambhir, Viktor Kunčak. VMCAI 2024.
- Differentiable Inductive Logic Programming in High-Dimensional Space, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCLR 2024, September 20th-22th 2024.
- Learning Rules Explaining Interactive Theorem Proving Tactic Prediction, Liao Zhang, David M. Cerna, Cezary Kaliszyk, IJCLR 2024, September 20th-22th 2024.
- Equational Anti-Unification over Absorption Theories, Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia, IJCAR 2024, July 1st-6th 2024.
- Learning Guided Automated Reasoning: A Brief Survey, Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban, Logics and Type Systems in Theory and Practice 2024.
- Generalisation through Negation and Predicate Invention, David M. Cerna and Andrew Cropper, AAAI-24, Feb. 22-25.
- A Sound and Complete Substitution Algorithm for Multimode Type Theory. Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. 2024. In 29th International Conference on Types for Proofs and Programs (TYPES 2023) (Leibniz International Proceedings in Informatics (LIPIcs)), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 4:1-4:23.
- Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDX, M. U. Sardar, T. Fossati, S. Frost, S. Xiong, IEEE Access, pp. 361-381, vol 12.
- Translating HOL-Light proofs to Coq, Frédéric Blanqui, 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR).
- Sharing proofs with predicative theories through universe-polymorphic elaboration, Thiago Felicissimo and Frédéric Blanqui, Logical Methods in Computer Science, Volume 20, Issue 3.
- Maude2Lean: Theorem proving for Maude specifications using Lean, Rubén Rubio and Adrián Riesco, JLAMP
- Comodule Representations of Second-Order Functionals, Danel Ahman and Andrej Bauer
- Transpension: The Right Adjoint to the Pi-type. Andreas Nuyts and Dominique Devriese. 2024. Logical Methods in Computer Science Volume 20, Issue 2, (June 2024).
- Kuroda’s Translation for the λΠ-Calculus Modulo Theory and Dedukti, Thomas Traversié, Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024).
- Proofs for Free in the λΠ-Calculus Modulo Theory, Thomas Traversié, Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024).
- Internal and Observational Parametricity for Cubical Agda. Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. 2024. Proc. ACM Program. Lang. 8, POPL (January 2024).
- The MoXI Model Exchange Tool Suite, Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier, CAV 2024
- Satisfiability Modulo Theories: A Beginner’s Tutorial, Clark W. Barrett, Cesare Tinelli, HanielBarbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar. FM 2024
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry, David Braun, NicolasMagaud, Pascal Schreck, JAR 2024.
- Automatic Verification of SMT Rewrites in Isabelle/HOL, Hanna Lachnitt and Mathias Fleury and Leni Aniva and Andrew Reynolds and Haniel Barbosa and Andres Nötzli and Clark W. Barrett and Cesare Tinelli. TACAS 2024.
- Certifying Incremental SAT Solving, Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere. LPAR 2024.
- A Modular Formalization of Superposition in Isabelle/HOL, Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret. ITP 2024.
- HOL Light to Isabelle/HOL Translation, Rebooted, Ghilain Bergeron, Stéphane Glondu and Sophie Tourret. Isabelle workshop 2024.
- Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract), Bruno Andreotti and Haniel Barbosa and Oliver Flatt. PAAR 2024.
- Who finds the short proof?. Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe. Log. J. IGPL 2024.
- The New TPTP Format for Interpretations. Geoff Sutcliffe, Alexander Steen, Pascal Fontaine.
2023
- Logic Operators and Quantifiers in Type-Theory of Algorithms, Roussanka Loukanova, Logic and Engineering of Natural Language Semantics (LENLS) 2022, LNCS 14213.
- CICM’22 System Entries, P. Koepke, A. Lorenzen, B. Shminke, Intelligent Computer Mathematics. CICM 2022. Lecture Notes in Computer Science, vol 13467.
- Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL, Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. Journal of Automated Reasoning, volume 67, Article number: 2 (2023).
- A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’23), January 16–17, 2023, Boston, MA, USA. ACM, New York, NY, USA.
- Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos, WoLLIC’23
- A Rewriting Coherence Theorem with Applications in Homotopy Type Theory, Nicolai Kraus, Jakob von Raumer, MSCS
- A Semantics of 𝕂 into Dedukti, Amélie Ledein, Valentin Blot, Catherine Dubois, TYPES’22
- A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, François Thiré, LMCS
- Admissible Types-to-PERs Relativizations in Higher-Order Logic, Andrei Popescu, Dmitriy Traytel, POPL’23
- An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format, Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa, TACAS’23
- An Interactive Interpretation Viewer for Typed First-order Logic, Jack McKeown, Geoff Sutcliffe, FLAIRS’23
- Anti-unification and Generalization: A Survey, David M. Cerna, Temur Kutsia, IJCAI’23
- Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving, Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux, ADG’23
- B-systems and C-systems are equivalent, Benedikt Ahrens, Jacopo Emmenegger, Paige R. North, Egbert Rijke, JSL
- Bases of pseudocompact Bishop spaces, Iosif Petrakis, Handbook of Constructive Mathematics
- Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition, Andreea Postovan, Mădălina Eraşcu, FROM’23
- Capturing constrained constructor patterns in matching logic, Xiaohong Chen, Dorel Lucanu, Grigore Roşu, JLAMP
- Certified Compilation of Choreographies with hacc, Luís Cruz-Filipe, Lovro Lugovic, Fabrizio Montesi, FORTE’23
- Combining Higher-Order Logic with Set Theory Formalizations, Cezary Kaliszyk, Karol Pąk, JAR
- Competition on Software Verification and Witness Validation: SV-COMP 2023, Dirk Beyer, TACAS’23
- Composable partial multiparty session types for open systems, Claude Stolze, Marino Miculan, Pietro Di Gianantonio, SoSyM
- Currying Order and Restricted Algorithmic Beta-Conversion in Type Theory of Acyclic Recursion, Roussanka Loukanova, Logically Speaking. A Festschrift for Marie Duzi
- Eta-Reduction in Type-Theory of Acyclic Recursion, Roussanka Loukanova, ADCAIJ
- Evasiveness Through Binary Decision Diagrams, Jesús Aransay, Laureano Lambán, Julio Rubio, CICM’23
- Experiments on Infinite Model Finding in SMT Solving, Julian Parsert, Chad Brown, Mikolas Janota, Cezary Kaliszyk, LPAR’23
- Exploring Mathematical Conjecturing with Large Language Models, Moa Johansson, Nicholas Smallbone, NeSy’23
- Extending a High-Performance Prover to Higher-Order Logic, Petar Vukmirović, Jasmin Blanchette, Stephan Schulz, TACAS’23
- Flexible Automation of Quantified Multi-Modal Logics with Interaction, Melanie Taprogge, Alexander Steen, KI’23
- For the Metatheory of Type Theory, Internal Sconing Is Enough, Rafaël Bocquet, Ambrus Kaposi, Christian Sattler, FSCD’23
- Formula Normalizations in Verification, Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kunčak, CAV’23
- Hammering Floating-Point Arithmetic, Olle Torstensson, Tjark Weber, FroCoS’23
- Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses, Taichi Uemura, FSCD’23
- How to frame innovation in mathematics, Bernhard Fisseni, Deniz Sarikaya, Bernhard Schröder, Synthese
- Keep me out of the loop: a more flexible choreographic projection, Luís Cruz-Filipe, Fabrizio Montesi, Robert R. Rasmussen, LPAR’23
- LISA: A Modern Proof System, Simon Guilloud, Sankalp Gambhir, Viktor Kunčak, ITP’23
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving, Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban, FroCoS’23
- Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users, Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann, ITP’23
- Matching-Logic-Based Understanding of Polynomial Functors and their Initial/Final Models, Dorel Lucanu, FROM’23
- Measuring the Readability of Geometric Proofs—The Area Method Case, Pedro Quaresma, Pierluigi Graziani, JAR
- Mechanising Gödel–Löb Provability Logic in HOL Light, Marco Maggesi, Cosimo Perini Brogi, JAR
- MizAR 60 for Mizar 50, Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban, ITP’23
- Multiple Query Satisfiability of Constrained Horn Clauses, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, PADL’23
- Now It Compiles! Certified Automatic Repair of Uncompilable Protocols, Luís Cruz-Filipe, Fabrizio Montesi, ITP’23
- On modified Halpern and Tikhonov-Mann iterations, Horațiu Cheval, Ulrich Kohlenbach, Laurentiu Leustean, J. Optim. Theor. Appl.
- Operationally-based program equivalence proofs using LCTRSs, Ştefan Ciobâcă, Dorel Lucanu, Andrei Sebastian Buruiană, JLAMP
- Parameterized Algebraic Protocols, Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos, PLDI’23
- Program Synthesis in Saturation, Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov, CADE-29
- Proof-carrying parameters in certified symbolic execution, Andrei Arusoaie, Dorel Lucanu, LJIGPL
- Propositional Forms of Judgemental Interpretations, Tao Xue, Zhaohui Luo, Stergios Chatzikyriakidis, J. Log. Lang. Inf.
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment, Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier, CADE’23
- Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Laurentiu Leustean, Pedro Pinto, Optimization Letters
- Reconstruction of TLAPS Proofs Solved by VeriT in Lambdapi, Coltellacci Alessio, ABZ’23
- Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic, Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown, LPAR’23
- Restricted Computations and Parameters in Type-Theory of Acyclic Recursion, Roussanka Loukanova, ADCAIJ
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Maria Paola Bonacina, Sarah Winkler, JAR
- Set-Theoretic and Type-Theoretic Ordinals Coincide, Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, LICS’23
- Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas, William M. Farmer
- Solving Modal Logic Problems by Translation to Higher-order Logic, Alexander Steen, Geoff Sutcliffe, Tobias Scholl, Christoph Benzmüller, CLAR’23
- Solving the SPARQL query containment problem with SpeCS, Mirko Spasić, Milena Vujošević Janičić, J. Web Semant.
- Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models, Alex Abuin, Alexander Bolotov, Montserrat Hermo, Paqui Lucio, JLAMP
- Tableaux for Realizability of Safety Specifications, Montserrat Hermo, Paqui Lucio, César Sánchez, FM’23
- Terms for Efficient Proof Checking and Parsing, Michael Färber, CPP’23
- Towards an Automatic Proof of the Bakery Algorithm, Aman Goel, Stephan Merz, Karem A. Sakallah, FORTE’23
- Translating proofs from an impredicative type system to a predicative one, Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal, CSL’23
- Two-level type theory and applications, Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler, MSCS
- Type-theoretic approaches to ordinals, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, TCS
- Verification of mutable linear data structures and iterator-based algorithms in Dafny, Jorge Blázquez, Manuel Montenegro, Clara Segura, JLAMP
- Verification of the ROS NavFn planner using executable specification languages, Enrique Martín, Manuel Montenegro, Adrián Riesco, Juan Rodríguez-Hortalá, Rubén Rubio, JLAMP
- VizAR: Visualization of Automated Reasoning Proofs &endash; System Description, Jan Jakubův, Cezary Kaliszyk, CICM’23
- Who Finds the Short Proof? An Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers, Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe. LJIGPL
- Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos. WoLLIC 2023, Lecture Notes in Computer Science, vol 13923. Springer.
2022
- Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022 - Issue 2, pages 401-412.
- Formalising Ordinal Partition Relations Using Isabelle/HOL, Mirna Džamonja, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022 - Issue 2, pages 383-400.
- Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs, Fabian Huch, In International Conference on Intelligent Computer Mathematics.
- Re-imagining the Isabelle Archive of Formal Proofs, MacKenzie, C., Huch, F., Vaughan, J., and Fleuriot, J. In International Conference on Intelligent Computer Mathematics.
- A Matching Logic Foundation for Alk, Alexandru-Ioan Lungu, Dorel Lucanu, ICTAC’22
- A Metatheoretic Analysis of Subtype Universes, Felix Bradley, Zhaohui Luo, TYPES’22
- Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo, FSCD’22
- Algebras of complemented subsets, Iosif Petrakis, Daniel Wessel, CiE’22
- Algorithmic Dependent-Type Theory of Situated Information and Context Assessments, Roussanka Loukanova, DCAI’22
- An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning, Alexander Steen, PAAR’22
- An Implementation of Set Theory with Pointed Graphs in Dedukti, Valentin Blot, Gilles Dowek, Thomas Traversié, LFMTP’22
- An extensible equality checking algorithm for dependent type theories, Andrej Bauer, Anja Petkovic Komel, LMCS
- Analysis and Transformation of Constrained Horn Clauses for Program Verification, Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti, TPLP
- Automated Reasoning in Non-classical Logics in the TPTP World, Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller, PAAR’22
- Automated Synthesis of Software Contracts with KINDSPEC, María Alpuente, Alicia Villanueva. Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems. Lecture Notes in Computer Science, volume 13160, Springer.
- Bécassine à la chasse au Coq, Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial, JFLA’22
- Bridging between LegalRuleML and TPTP for Automated Normative Reasoning, Alexander Steen, David Fuenmayor, RuleML+RR’22
- CDSAT for nondisjoint theories with shared predicates: arrays with abstract length, Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar, SMT’22
- Closed subsets in Bishop topological groups, Iosif Petrakis, TCS
- Computability models over categories and presheaves, Iosif Petrakis, LFCS’22
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar, JAR
- Contract Strengthening through Constrained Horn Clause Verification, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, HCVS’22
- Contradiction Detection and Repair in Large Theories, Adam Pease, Stephan Schulz, FLAIRS’22
- Effective Kan Fibrations in Simplicial Sets, Benno van den Berg, Eric Faber
- Empirical Properties of Term Orderings for Superposition, Stephan Schulz, PAAR’22
- Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity, Frédéric Blanqui, FSCD’22
- Evolution of Automated Deduction and Dynamic Constructions in Geometry, Pedro Quaresma, Mathematics Education in the Age of Artificial Intelligence, 2022
- Formalizing Alexander duality through BDDs, Jesús Aransay, Laureano Lambán, Julius Michaelis, Julio Rubio, ISAIM’22
- Four Geometry Problems to Introduce Automated Deduction in Secondary Schools, Pedro Quaresma, Vanda Santos, ThEdu’21
- Larry Wos – Visions of automated reasoning, Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe, JAR
- Learning Higher-Order Logic Programs From Failures, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCAI’22
- Lemmaless Induction in Trace Logic, Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger, CICM’22
- Mechanizing Matching Logic In Coq, Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Lucas Peña, Jan Tušil, FROM’22
- On Quantitative Algebraic Higher-Order Theories, Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone, FSCD’22
- On SGGS and Horn clauses, Maria Paola Bonacina, Sarah Winkler, PAAR’22
- Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification, Andrei Arusoaie, Dorel Lucanu, FROM’22
- Proof-relevance in Bishop-style constructive mathematics, Iosif Petrakis, MSCS
- Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting, Michael Färber, CPP’22
- Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, J. Log. Comput
- Set of support, demodulation, paramodulation: a historical perspective, Maria Paola Bonacina, JAR
- Sikkel: Multimode Simple Type Theory as an Agda Library, Joris Ceulemans, Andreas Nuyts, Dominique Devriese, MSFP’22
- Strict computability models over categories and presheaves, Iosif Petrakis, J. Log. Comput.
- The Logic Languages of the TPTP World, Geoff Sutcliffe, LJIGPL
- Theorem Proving for Maude Specifications Using Lean, Rubén Rubio, Adrián Riesco, ICFEM’22
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses, Emanuele De Angelis, Maurizio Proietti, Fabio Fioravanti, Alberto Pettorossi, TPLP
- Vers une traduction de K en Dedukti (Towards a translation of K in Dedukti), Amélie Ledein, Valentin Blot, Catherine Dubois, JFLA’22
- What Can Formal Systems Do For Mathematics? A Discussion Through The Lens Of Proof Assistants: Some Recent Advances, Angeliki Koutsoukou-Argyraki Q&A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson, Special Issue for the 60th Anniversary of the DVMLG (German Association for Mathematical Logic and for Basic Research in the Exact Sciences), Benedikt Löwe, Deniz Sarikaya (eds.), College Publications, 2022
- A More Pragmatic {CDCL} for IsaSAT and Targetting {LLVM} (Short Paper). Mathias Fleury and Peter Lammich. CADE’29 (2023).
Reports
-
2nd WG3 meeting, Timisoara, 8-9 February 2023, slides&videos report
-
1st WG3 meeting, Valencia, 10-11 February 2022 slides&videos report