Parameterized synthesis for fragments of first-order logic over data words
From MaRDI portal
Publication:2200816
DOI10.1007/978-3-030-45231-5_6OpenAlexW3022817002MaRDI QIDQ2200816
Mathieu Lehaut, Nathalie Sznajder, Benedikt Bollig, Béatrice Bérard
Publication date: 23 September 2020
Full work available at URL: https://arxiv.org/abs/1910.14294
Related Items
Church synthesis on register automata over linearly ordered data domains, Realizability problem for constraint LTL
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Eisbach: a proof method language for Isabelle
- Isabelle/HOL. A proof assistant for higher-order logic
- Bridging the Gap: Automatic Verified Abstraction of C
- The Essence of Higher-Order Concurrent Separation Logic
- A Brief Overview of HOL4
- Communicating sequential processes
- Automated proofs of object code for a widely used microprocessor
- Compositional shape analysis by means of bi-abduction
- Computer Aided Verification
- Verification Condition Generation Via Theorem Proving
- CakeML
- A Decision Procedure for Bit-Vectors and Arrays
- An axiomatic basis for computer programming
- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
- Hoare Logic for Realistically Modelled Machine Code
- Classes of Recursively Enumerable Sets and Their Decision Problems
