CAV 2009 - PDF Preprint Papers

CAV 2009 International Workshop on Computer Aided Verification

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CAV-2009 Paper

click to vote

CAV
2009
Springer

239views Hardware» more CAV 2009»

MCMAS: A Model Checker for the Verification of Multi-Agent Systems

13 years 8 months ago

Download www.doc.ic.ac.uk

tic modalities for correctness [16]. The release described in this abstract is a complete rebuild of a preliminary experimental checker [14]. The model input language includes vari...

Alessio Lomuscio, Hongyang Qu, Franco Raimondi

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	239	MCMAS: A Model Checker for the Verification of Multi-Agent Systems	claim
2	218	Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers	claim
3	215	Homer: A Higher-Order Observational Equivalence Model checkER	claim
4	212	Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
5	209	Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers	claim
6	206	D-Finder: A Tool for Compositional Deadlock Detection and Verification	claim
7	187	A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints	claim
8	184	Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique	claim
9	182	Generalizing DPLL to Richer Logics	claim
10	181	Size-Change Termination, Monotonicity Constraints and Ranking Functions	claim
11	177	Software Transactional Memory on Relaxed Memory Models	claim
12	176	PAT: Towards Flexible Verification under Fairness	claim
13	171	CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs	claim
14	169	Automatic Verification of Integer Array Programs	claim
15	168	Games through Nested Fixpoints	claim
16	165	Symbolic Counter Abstraction for Concurrent Software	claim
17	165	Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences	claim
18	164	InvGen: An Efficient Invariant Generator	claim
19	163	Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories	claim
20	157	Explaining Counterexamples Using Causality	claim
21	156	Towards Performance Prediction of Compositional Models in Industrial GALS Designs	claim
22	155	The Zonotope Abstract Domain Taylor1+	claim
23	155	Better Quality in Synthesis through Quantitative Objectives	claim
24	153	Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep	claim
25	150	Automated Analysis of Java Methods for Confidentiality	claim
26	141	Apron: A Library of Numerical Abstract Domains for Static Analysis	claim
27	139	A Concurrent Portfolio Approach to SMT Solving	claim
28	138	Reducing Context-Bounded Concurrent Reachability to Sequential Reachability	claim
29	137	An Antichain Algorithm for LTL Realizability	claim
30	137	VS3: SMT Solvers for Program Verification	claim
31	136	Intra-module Inference	claim
32	136	Linear Functional Fixed-points	claim
33	135	Sliding Window Abstraction for Infinite Markov Chains	claim
34	134	Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints	claim
35	133	Cardinality Abstraction for Declarative Networking Applications	claim
36	132	Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion	claim
37	128	Modelling Epigenetic Information Maintenance: A Kappa Tutorial	claim
38	127	Incremental Instance Generation in Local Reasoning	claim
39	126	Reachability Analysis of Hybrid Systems Using Support Functions	claim
40	123	Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models	claim
41	123	On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure	claim
42	119	HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment	claim
43	116	Meta-analysis for Atomicity Violations under Nested Locking	claim
44	116	Priority Scheduling of Distributed Systems Based on Model Checking	claim
45	106	Models and Proofs of Protocol Security: A Progress Report	claim
46	105	Transactional Memory: Glimmer of a Theory	claim
47	104	SPEED: Symbolic Complexity Bound Analysis	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers