The Succinct Solver Suite offers two analysis engines for solving data and control flow problems expressed in clausal form in a large fragment of first-order logic. The solvers have proved to be useful for a variety of applications including security properties of Java Card byte-code, access control features of Mobile and Discretionary Ambients, and validation of protocol narrations formalised in a suitable process algebra. Both solvers operate over finite domains although they can cope with regular sets of trees by direct encoding of the tree grammars; they differ in fine details about the demands on the universe and the extent to which universal quantification is allowed. A number of transformation strategies, mainly automatic, have been studied aiming on the one hand to increase the efficiency of the solving process, and on the other hand to increase the ease with which users can develop analyses. The results from benchmarking against state-of-the-art solvers are encouraging.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- de Nicola, Rocco; Gorla, Daniele; Hansen, René Rydhof; Nielson, Flemming; Nielson, Hanne Riis; Probst, Christian W.; Pugliese, Rosario: From flow logic to static type systems for coordination languages (2010)
- Gordon, Andrew D.; Hüttel, Hans; Hansen, René Rydhof: Type inference for correspondence types (2009)
- Pilegaard, Henrik; Nielson, Flemming; Nielson, Hanne Riis: Pathway analysis for bioambients (2008)
- Nanz, Sebastian; Hankin, Chris: A framework for security analysis of mobile wireless networks (2006)
- Nanz, Sebastian; Hankin, Chris: Formal security analysis for ad-hoc networks. (2006)
- Keinänen, Misa: Obtaining memory-efficient solutions to Boolean equation systems. (2005)
- Nielson, Flemming; Nielson, Hanne Riis; Sun, Hongyan; Buchholtz, Mikael; Hansen, René Rydhof; Pilegaard, Henrik; Seidl, Helmut: The succinct solver suite (2004)