1.

Record Nr.

UNISA996465986303316

Titolo

Model Checking Software [[electronic resource] ] : 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings / / edited by Jaco van der Pol, Michael Weber

Pubbl/distr/stampa

Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010

ISBN

1-280-38959-1

9786613567512

3-642-16164-2

Edizione

[1st ed. 2010.]

Descrizione fisica

1 online resource (X, 263 p. 70 illus.)

Collana

Theoretical Computer Science and General Issues, , 2512-2029 ; ; 6349

Disciplina

005.1

Soggetti

Software engineering

Compilers (Computer programs)

Computer programming

Computer science

Machine theory

Software Engineering

Compilers and Interpreters

Programming Techniques

Computer Science Logic and Foundations of Programming

Formal Languages and Automata Theory

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

Note generali

Bibliographic Level Mode of Issuance: Monograph

Nota di bibliografia

Includes bibliographical references and index.

Nota di contenuto

Satisfiability Modulo Theories for Model Checking -- SMT-Based Software Model Checking -- Symbolic Object Code Analysis -- Model Checking in Context -- Experimental Comparison of Concolic and Random Testing for Java Card Applets -- Combining SPIN with ns-2 for Protocol Optimization -- Automatic Generation of Model Checking Scripts Based on Environment Modeling -- Implementation and Performance of Model Checking -- Model Checking: Cleared for Take Off -- Context-Enhanced Directed Model Checking -- Efficient Explicit-State Model Checking on General Purpose Graphics Processors



-- The SpinJa Model Checker -- LTL and Büchi Automata -- On the Virtue of Patience: Minimizing Büchi Automata -- Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance -- Nevertrace Claims for Model Checking -- Infinite State Models -- A False History of True Concurrency: From Petri to Tools -- Analysing Mu-Calculus Properties of Pushdown Systems -- Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains -- An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models -- Concurrent Software -- Context-Bounded Translations for Concurrent Software: An Empirical Evaluation -- One Stack to Run Them All.