Automatic proofs of protocols via program transformation

MaRDI QIDQ5701513zbMATH OpenFDO

Authors Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

Publication date 3 November 2005

zbMATH Keywords

multiagent system

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Learning and adaptive systems in artificial intelligence (68T05)

Recommendations

• Transformational Verification of Parameterized Protocols Using Array Formulas
• Automatic verification of temporal-epistemic properties of cryptographic protocols
• Verification of sets of infinite state processes using program transformation
• Unfold/fold transformations for automated verification of parameterized concurrent systems
• Logics in Artificial Intelligence

Cited in

(10)

• Using theorem proving to verify properties of agent programs
• Verifying Agents’ Conformance with Multiparty Protocols
• An extension of protocol verification modal logic to multi-channel protocols
• Constraint-based verification of client-server protocols
• Automated Synthesis of Protocol Converters with BALM-II
• Automatic verification of temporal-epistemic properties of cryptographic protocols
• Transformational Verification of Parameterized Protocols Using Array Formulas
• Abstract State Machines 2004. Advances in Theory and Practice
• Automatic Generation of Sources Lemmas in Tamarin: Towards Automatic Proofs of Security Protocols
• Proving the correctness of recursion-based automatic program transformations

This page was built for publication: Automatic proofs of protocols via program transformation

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