Paper Info
Title
Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems
Abstract
This paper presents Kiasan, a bounded technique to reason about open systems based on a path sensitive, relatively sound and complete symbolic execution instead of the usual compositional reasoning through weakest precondition calculation that summarizes all execution paths. Kiasan is able to check strong heap properties, and it is fully automatic and flexible in terms of its cost and the guarantees it provides. It allows a user-adjustable mixed compositional/non-compositional reasoning and naturally produces error traces as fault evidence. We implemented Kiasan using the Bogor model checking framework and observed that its performance is comparable to ESC/Java on similar scales of problems and behavioral coverage, while providing the ability to check much stronger specifications
Year
DOI
Venue
2006
10.1109/ASE.2006.26
ASE
Keywords
Field
DocType
non-compositional reasoning,open systems,error trace,heap property checking,noncompositional reasoning,execution path,bounded technique,compositional reasoning,bogor model checking framework,k-bounded symbolic execution,behavioral coverage,reasoning about programs,complete symbolic execution,open system,fault diagnosis,program diagnostics,usual compositional reasoning,kiasan technique,fault evidence,specification checking,bogor model checking,error traces,formal specification,strong heap properties,model checking
Predicate transformer semantics,Programming language,Model checking,Computer science,Theoretical computer science,Heap (data structure),Formal specification,Symbolic execution,Open system (systems theory),Java,Bounded function
Conference
ISSN
ISBN
Citations 
1938-4300
0-7695-2579-2
61
PageRank 
References 
Authors
2.52
16
3
Name
Order
Citations
PageRank
Xianghua Deng117011.13
Jooyong Lee2612.52
Robby31489104.82