Verification from Declarative Specifications Using Logic Programming

DOI10.1007/978-3-540-89982-2_39zbMATH Open1185.68419OpenAlexW1514325465WikidataQ57977956 ScholiaQ57977956MaRDI QIDQ5504672FDOQ5504672

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

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

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

Recommendations

• Verification of logic programs
• Logic programs as specifications in the inductive verification of logic programs
• scientific article; zbMATH DE number 1497823
• Abstract interpretation based verification of logic programs
• scientific article; zbMATH DE number 1973214
• Assertion based inductive verification methods for logic programs
• scientific article; zbMATH DE number 1926608
• scientific article; zbMATH DE number 3907752
• Specifying, programming and verifying with equational logic

Cites Work

• scientific article; zbMATH DE number 88991 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2090517 (Why is no real title available?)
• ${\cal B}$ -Tropos
• A resolution principle for constrained logics
• Abductive Logic Programming
• Algorithm = logic + control
• Clausal temporal resolution
• Coinductive Logic Programming and Its Applications
• Logic Programming
• NuSMV: A new symbolic model checker
• Real-time logics: Complexity and expressiveness
• Theory and practice of constraint handling rules
• Verifiable agent interaction in abductive logic programming: the SCIFF framework

Cited In (17)

• Business process verification with constraint temporal answer set programming
• Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation
• Foundations of declarative testing in arbitrary logic programming
• On the integration of declarative choreographies and Commitment-based agent societies into the SCIFF logic programming framework
• Title not available (Why is no real title available?)
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• Deductive verification in decidable fragments with Ivy
• Verifying Agents’ Conformance with Multiparty Protocols
• Specification and verification of declarative open interaction models. A logic-based approach
• Abductive logic programming as an effective technology for the static verification of declarative business processes
• Exception diagnosis in multiagent contract executions
• Logics and automata for verification: Expressiveness and decidability issues
• Title not available (Why is no real title available?)
• Where logic and agents meet
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)

Uses Software

• HYPROLOG
• NuSMV
• Uppaal
• SCIFF

This page was built for publication: Verification from Declarative Specifications Using Logic Programming

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