Verification of composed array-based systems with applications to security-aware workflows

DOI10.1007/978-3-642-40885-4_4MaRDI QIDQ2849480zbMATH OpenOpenAlexFDO

Authors Clara Bertolissi, Silvio Ranise

Publication date 20 September 2013

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-40885-4_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Towards SMT Model Checking of Array-Based Systems
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
• Specifying and verifying secrecy in workflows with arbitrarily many agents
• Ensuring completeness of symbolic verification methods for infinite-state systems

Cited in

(1)

• Theoretical Computer Science

Describes a project that uses

Uses Software

• Cubicle
• Mcmt

This page was built for publication: Verification of composed array-based systems with applications to security-aware workflows

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