Synthesis and compositional verification using language learning

Keywords

Computer science, Correctness, Model checking, Programming language, Oracle

References

• UCPOP: A Sound, Complete, Partial Order Planner for ADLJ. Scott Penberthy, Daniel S. Weld — 1992
• Reasoning about Actions and Planning in LTL Action TheoriesDiego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi — 2002
• Planning with Incomplete Information as Heuristic Search in Belief SpaceBlai Bonet, Héctor Geffner — 2000
• A Framework for Planning with Extended Goals under Partial ObservabilityPiergiorgio Bertoli, Alessandro Cimatti, Marco Pistore — 2003
• Planning as Model Checking for Extended Goals in Non-deterministic DomainsMarco Pistore, Paolo Traverso — 2001
• 2Planning for Contingencies: A Decision-based ApproachL. Pryor, Gregg Collins — 1996
• TALplanner: A temporal logic based forward chaining plannerJonas Kvarnström, Patrick Doherty — 2001
• Planning with Extended Goals and Partial ObservabilityPiergiorgio Bertoli, Marco Pistore — 2004
• Planning for temporally extended goalsFahiem Bacchus, Froduald Kabanza — 1996
• Conditional progressive planning under uncertaintyLars Karlsson — 2001
• Black Box CheckingDoron Peled, Moshe Y. Vardi, Mihalis Yannakakis — 1999
• Planning in Nondeterministic Domains under Partial Observability via Symbolic Model CheckingPiergiorgio Bertoli, Alessandro Cimatti, Marco Roveri — 2001
• Proof Rules for Automated Compositional Verification through LearningHoward Barringer, Dimitra Giannakopolou, Corina S. Păsăreanu — 2003
• Modern Operating SystemsAndrew S. Tanenbaum — 1992
• The Temporal Semantics of Concurrent ProgramsAmir Pnueli — 1979
• Software model checking: extracting verification models from source code †Gerard J. Holzmann, Margaret Smith — 2001
• Planning Control Rules for Reactive AgentsF. Kabanza, Michel Barbeau, Richard St‐Denis — 1997
• Learning Regular Sets from Queries and CounterexamplesDana Angluin — 1987
• Weak, strong, and strong cyclic planning via symbolic model checkingAlessandro Cimatti, Marco Pistore, Marco Roveri — 2003
• Enforcing high-level protocols in low-level softwareRobert DeLine, Manuel Fähndrich — 2001

Cited by

No citing papers recorded for this paper.

Related papers

• Probabilistic symbolic model checking with engineering models and applicationsVasiliki Hartonas-Garmhausen — 1998
• On Implementation of the Improved Assume-Guarantee Verification Method for Timed SystemsHoang-Viet Tran, Quang-Trung Nguyen, Phạm Ngọc Hùng — 2019
• Automated circular assume-guarantee reasoningKaram Abd Elkader, Orna Grümberg, Corina S. Păsăreanu — 2015
• Automatic generation of invariants in formal verification of microprocessors and memory systemsDavid L. Dill, Husam Abu-Haimed — 2004
• Verification of Erlang Programs using Testing and TracingH. Svensson — 2005
• What is formal verification?Per Bjesse — 2005
• Model checking temporal knowledge and commitments in multi-agent systems using reductionFaisal Al-Saqqar, Jamal Bentahar, Khalid Sultan — 2015
• Foundations for the run-time analysis of software systemsMahesh Viswanathan, Sampath Kannan, Insup Lee — 2000