Titlebook: Verified Software: Theories, Tools and Experiments; 6th International Co Dimitra Giannakopoulou,Daniel Kroening Conference proceedings 2014

CLOUT

Diastole

LURE

Certification of Nontermination Proofs Using Strategies and Nonlooping Derivationsrategies include (an extended version of) forbidden patterns, which cover in particular outermost and context-sensitive rewriting. Finally, a mechanism to support partial nontermination proofs further extends the applicability of our proof checker.

加剧

1FAWN

Using Promela in a Fully Verified Executable LTL Model Checkertion of the Promela semantics within Isabelle, which is used both to define the semantics and to automatically generate code for the computation of the state space. We report on experiments on standard Promela benchmarks comparing our tool to SPIN.

Accrue

不可思议

Conference proceedings 2014re organized in topical sections such as analysis: understanding and explanation; verification frameworks and applications; hypervisors and dynamic data structures; certification; real time and security.

额外的事

有害

hysterectomy

Efficient Refinement Checking in VCCcation tool. The main idea is to first perform a systematic translation from the top-level abstract model to a ghost implementation in VCC. Subsequent refinement proofs between successively refined abstract models and between abstract and concrete implementations are carried out in VCC. We propose a