Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
From MaRDI portal
Publication:2441771
DOI10.1007/s10703-012-0157-1zbMath1284.68520MaRDI QIDQ2441771
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
symbolic model checking; SMT solving; security analysis of administrative role-based access control policies
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
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