Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
From MaRDI portal
Publication:2441771
DOI10.1007/s10703-012-0157-1zbMath1284.68520OpenAlexW1484683107MaRDI 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 checkingSMT solvingsecurity analysis of administrative role-based access control policies
Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
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