Titlebook: Verification, Model Checking, and Abstract Interpretation; 10th International C Neil D. Jones,Markus Müller-Olm Conference proceedings 2009

皮萨

An Abort-Aware Model of Transactional Programmingd transactions, transactions which may never terminate, and transactions which may be aborted explicitly, or aborted automatically by the run-time environment due to memory conflicts..We show that concurrent executions of TSMs satisfy a correctness criterion closely related to serializability, which

嬉耍

LVAD360

Query-Driven Program Testing, and strengthens the clause database with additional clauses which exclude redundant new solutions. We demonstrate the scalability of our approach and its ability to compute compact test suites with experiments involving device drivers, automotive controllers, and open source projects.

蘑菇

Conference proceedings 2009ystems, deductive methods, and optimization. The Program Committee selected 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguis

DAMP

Mark Kattenbelt,Marta Kwiatkowska,Gethin Norman,David Parker

obeisance

Nicholas Kidd,Thomas Reps,Julian Dolby,Mandana Vaziri

描述

Verification, Model Checking, and Abstract Interpretation10th International C

让你明白

Model-Checking the Linux Virtual File Systembility of retrospective verification of a VFS implementation using model-checking technology. We show how to extract an executable model of the Linux VFS implementation, validate the model by employing the simulation capabilities of SPIN, and analyse it for adherence to data integrity constraints and deadlock freedom using the SMART model checker.

Bouquet

Legion

Monitoring the Full Range of ,-Regular Properties of Stochastic Systemspplication with probabilities and also a Streett automaton that specifies the property to be monitored. It generates a monitor for monitoring computations of the application. Experimental results comparing the effectiveness of the different algorithms are presented.