Symbolic backward reachability with effectively propositional logic. Application to security policy analysis

DOI10.1007/s10703-012-0157-1zbMath1284.68520MaRDI QIDQ2441771

Silvio Ranise

Publication date: 28 March 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0157-1

zbMATH Keywords

symbolic model checking; SMT solving; security analysis of administrative role-based access control policies

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

68Q60: Specification and verification (program logics, model checking, etc.)

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Uses Software

• RBAC-PAT
• TPTP
• ASASP
• Mcmt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Policy analysis for administrative role-based access control
• Combining nonstably infinite theories
• Complexity results for classes of quantificational formulas
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Access Nets: Modeling Access to Physical Spaces
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• MCMT: A Model Checker Modulo Theories