Realizability modulo theories

DOI10.1016/J.JLAMP.2024.100971MaRDI QIDQ6561346zbMATH OpenFDO

Authors Andoni Rodríguez, César Sánchez

Publication date 25 June 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2024.100971

zbMATH Keywords

Boolean abstractionfirst-order theoriesLTL modulo theoriesreactive synthesisSMT solving

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• A constraint-based approach to solving games on infinite graphs
• A Decision Procedure for the First Order Theory of Real Addition with Order
• A new decision method for elementary algebra
• Alfred Tarski's elimination theory for real closed fields
• Automata, logics, and infinite games. A guide to current research
• Boolean abstractions for realizability modulo theories
• Bounded synthesis of register transducers
• Causality-based game solving
• Church’s Problem and a Tour through Automata Theory
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Definability and decision problems in arithmetic
• scientific article; zbMATH DE number 3755842 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1157649 (Why is no real title available?)
• scientific article; zbMATH DE number 1157651 (Why is no real title available?)
• scientific article; zbMATH DE number 1954378 (Why is no real title available?)
• scientific article; zbMATH DE number 3895043 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 3273189 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• LTL with arithmetic and its applications in reasoning about hierarchical systems
• On synthesis of specifications with arithmetic
• Reactive synthesis from signal temporal logic specifications
• Synthesis of Reactive(1) designs
• Synthesis with Identifiers
• Temporal stream logic modulo theories
• Temporal stream logic: synthesis beyond the Bools
• Vacuity in synthesis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(2)

• Preface to selected papers from 21st workshop on programming and languages (PROLE 2022)
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures

This page was built for publication: Realizability modulo theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6561346)