Verification from Declarative Specifications Using Logic Programming

DOI10.1007/978-3-540-89982-2_39zbMath1185.68419OpenAlexW1514325465WikidataQ57977956 ScholiaQ57977956MaRDI QIDQ5504672

Federico Chesani, Marco Alberti, Paolo Torroni, Evelina Lamma, Paola Mello, Marco Montali, Marco Gavanelli

Publication date: 22 January 2009

Published in: Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-89982-2_39

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Related Items

Exception diagnosis in multiagent contract executions ⋮ Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation ⋮ Where logic and agents meet ⋮ Verifying Agents’ Conformance with Multiparty Protocols ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models

Uses Software

• HYPROLOG
• NuSMV
• Uppaal
• SCIFF

Cites Work

• Real-time logics: Complexity and expressiveness
• A resolution principle for constrained logics
• NuSMV: A new symbolic model checker
• ${\cal B}$ -Tropos
• Coinductive Logic Programming and Its Applications
• Algorithm = logic + control
• Theory and practice of constraint handling rules
• Verifiable agent interaction in abductive logic programming
• Abductive Logic Programming
• Logic Programming
• Clausal temporal resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item