Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
25 Years of Model Checking [[electronic resource] ] : History, Achievements, Perspectives / / edited by Orna Grumberg, Helmut Veith
| 25 Years of Model Checking [[electronic resource] ] : History, Achievements, Perspectives / / edited by Orna Grumberg, Helmut Veith |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (VII, 234 p.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Computer programming Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Programming Techniques Formal Languages and Automata Theory |
| ISBN | 3-540-69850-7 |
| Classificazione |
DAT 003f
DAT 325f DAT 540f SS 4800 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Birth of Model Checking -- The Beginning of Model Checking: A Personal Perspective -- Verification Technology Transfer -- New Challenges in Model Checking -- A Retrospective on Mur? -- Model Checking: From Tools to Theory -- Value Iteration -- Fifteen Years of Formal Property Verification in Intel -- A View from the Engine Room: Computational Support for Symbolic Model Checking -- From Church and Prior to PSL -- On the Merits of Temporal Testers -- DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC -- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR. |
| Record Nr. | UNISA-996465393403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
25 years of model checking : history, achievements, perspectives / / Orna Grumberg, Helmut Veith (eds.)
| 25 years of model checking : history, achievements, perspectives / / Orna Grumberg, Helmut Veith (eds.) |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2008 |
| Descrizione fisica | 1 online resource (VII, 234 p.) |
| Disciplina | 005.131 |
| Altri autori (Persone) |
GrumbergOrna
VeithHelmut |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico | Computer systems - Verification |
| ISBN | 3-540-69850-7 |
| Classificazione |
DAT 003f
DAT 325f DAT 540f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Birth of Model Checking -- The Beginning of Model Checking: A Personal Perspective -- Verification Technology Transfer -- New Challenges in Model Checking -- A Retrospective on Mur? -- Model Checking: From Tools to Theory -- Value Iteration -- Fifteen Years of Formal Property Verification in Intel -- A View from the Engine Room: Computational Support for Symbolic Model Checking -- From Church and Prior to PSL -- On the Merits of Temporal Testers -- DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC -- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR. |
| Altri titoli varianti | Twenty-five years of model checking |
| Record Nr. | UNINA-9910767508103321 |
| Berlin, : Springer, 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis [[electronic resource] ] : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn
| Automated Technology for Verification and Analysis [[electronic resource] ] : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XI, 414 p.) |
| Disciplina | 004n/a |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computers
Computer programming Programming languages (Electronic computers) Computer logic Mathematical logic Algorithms Theory of Computation Programming Techniques Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Algorithm Analysis and Problem Complexity |
| Soggetto genere / forma |
Kongress.
Macao (2009) |
| ISBN | 3-642-04761-0 |
| Classificazione |
DAT 286f
DAT 325f DAT 704f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Verifying VLSI Circuits -- 3-Valued Abstraction for (Bounded) Model Checking -- Local Search in Model Checking -- State Space Reduction -- Exploring the Scope for Partial Order Reduction -- State Space Reduction of Linear Processes Using Control Flow Reconstruction -- A Data Symmetry Reduction Technique for Temporal-epistemic Logic -- Tools -- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets -- CLAN: A Tool for Contract Analysis and Conflict Discovery -- UnitCheck: Unit Testing and Model Checking Combined -- Probabilistic Systems -- LTL Model Checking of Time-Inhomogeneous Markov Chains -- Statistical Model Checking Using Perfect Simulation -- Quantitative Analysis under Fairness Constraints -- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems -- Medley -- Memory Usage Verification Using Hip/Sleek -- Solving Parity Games in Practice -- Automated Analysis of Data-Dependent Programs with Dynamic Memory -- Temporal Logic I -- On-the-fly Emptiness Check of Transition-Based Streett Automata -- On Minimal Odd Rankings for Büchi Complementation -- Specification Languages for Stutter-Invariant Regular Properties -- Abstraction and Refinement -- Incremental False Path Elimination for Static Software Analysis -- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement -- Don’t Know for Multi-valued Systems -- Logahedra: A New Weakly Relational Domain -- Fault Tolerant Systems -- Synthesis of Fault-Tolerant Distributed Systems -- Formal Verification for High-Assurance Behavioral Synthesis -- Dynamic Observers for the Synthesis of Opaque Systems -- Temporal Logic II -- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation -- LTL Model Checking for Recursive Programs -- On Detecting Regular Predicates in Distributed Systems. |
| Record Nr. | UNISA-996465383803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009 ; Proceedings / / Zhiming Liu, Anders P. Ravn (eds.)
| Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009 ; Proceedings / / Zhiming Liu, Anders P. Ravn (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer-Verlag, c2009 |
| Descrizione fisica | 1 online resource (XI, 414 p.) |
| Disciplina | 004n/a |
| Altri autori (Persone) |
LiuZhiming <1961->
RavnAnders P |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Artificial intelligence
Automatic theorem proving |
| ISBN | 3-642-04761-0 |
| Classificazione |
DAT 286f
DAT 325f DAT 704f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Verifying VLSI Circuits -- 3-Valued Abstraction for (Bounded) Model Checking -- Local Search in Model Checking -- State Space Reduction -- Exploring the Scope for Partial Order Reduction -- State Space Reduction of Linear Processes Using Control Flow Reconstruction -- A Data Symmetry Reduction Technique for Temporal-epistemic Logic -- Tools -- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets -- CLAN: A Tool for Contract Analysis and Conflict Discovery -- UnitCheck: Unit Testing and Model Checking Combined -- Probabilistic Systems -- LTL Model Checking of Time-Inhomogeneous Markov Chains -- Statistical Model Checking Using Perfect Simulation -- Quantitative Analysis under Fairness Constraints -- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems -- Medley -- Memory Usage Verification Using Hip/Sleek -- Solving Parity Games in Practice -- Automated Analysis of Data-Dependent Programs with Dynamic Memory -- Temporal Logic I -- On-the-fly Emptiness Check of Transition-Based Streett Automata -- On Minimal Odd Rankings for Büchi Complementation -- Specification Languages for Stutter-Invariant Regular Properties -- Abstraction and Refinement -- Incremental False Path Elimination for Static Software Analysis -- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement -- Don’t Know for Multi-valued Systems -- Logahedra: A New Weakly Relational Domain -- Fault Tolerant Systems -- Synthesis of Fault-Tolerant Distributed Systems -- Formal Verification for High-Assurance Behavioral Synthesis -- Dynamic Observers for the Synthesis of Opaque Systems -- Temporal Logic II -- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation -- LTL Model Checking for Recursive Programs -- On Detecting Regular Predicates in Distributed Systems. |
| Altri titoli varianti | ATVA 2009 |
| Record Nr. | UNINA-9910484140503321 |
| Berlin ; ; Heidelberg, : Springer-Verlag, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : foundations and applications ; 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 ; revised selected papers / / Marcel Vinicius Medeiros Oliveira, Jim Woodcock (eds.)
| Formal methods : foundations and applications ; 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 ; revised selected papers / / Marcel Vinicius Medeiros Oliveira, Jim Woodcock (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | New York ; ; Berlin, : Springer, c2009 |
| Descrizione fisica | 1 online resource (X, 351 p.) |
| Disciplina | 004 |
| Altri autori (Persone) |
OliveiraMarcel Vinicius Medeiros
WoodcockJim |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Formal methods (Computer science)
Electronic data processing |
| ISBN | 3-642-10452-5 |
| Classificazione |
DAT 310f
DAT 325f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Speeding Up Simulation of SystemC Using Model Checking -- Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering -- Satisfiability Modulo Theories: An Appetizer -- Interruption Testing of Reactive Systems -- Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS -- Concurrent Models of Flash Memory Device Behaviour -- Corecursive Algebras: A Study of General Structured Corecursion -- Formalizing FreeRTOS: First Steps -- A Mechanized Strategy for Safe Abstraction of CSP Specifications -- Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B -- An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model -- Towards Safe Design of Synchronous Bus Protocols in Event-B -- Mechanising Data-Types for Kernel Design in Z -- A Complete Set of Object Modeling Laws for Alloy -- Undecidability Results for Distributed Probabilistic Systems -- Formalisation and Analysis of Objects as CSP Processes -- Concolic Testing of the Multi-sector Read Operation for Flash Memory File System -- Low-Level Code Verification Based on CSP Models -- Formal Modelling of a Microcontroller Instruction Set in B -- Defining Behaviours by Quasi-finality -- Verifying Compiled File System Code -- Reasoning about General Quantum Programs over Mixed States -- A Simple and General Theoretical Account for Abstract Types. |
| Record Nr. | UNINA-9910483264203321 |
| New York ; ; Berlin, : Springer, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Methods: Foundations and Applications [[electronic resource] ] : 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers / / edited by Marcel Vinícius Medeiros Oliveira, Jim Woodcock
| Formal Methods: Foundations and Applications [[electronic resource] ] : 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers / / edited by Marcel Vinícius Medeiros Oliveira, Jim Woodcock |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (X, 351 p.) |
| Disciplina | 004 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computers Computer logic Computer programming Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Theory of Computation Software Engineering Logics and Meanings of Programs Programming Techniques |
| Soggetto genere / forma |
Gramado (2009)
Kongress (2009) Kongress. Online-Publikation |
| ISBN | 3-642-10452-5 |
| Classificazione |
DAT 310f
DAT 325f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Speeding Up Simulation of SystemC Using Model Checking -- Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering -- Satisfiability Modulo Theories: An Appetizer -- Interruption Testing of Reactive Systems -- Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS -- Concurrent Models of Flash Memory Device Behaviour -- Corecursive Algebras: A Study of General Structured Corecursion -- Formalizing FreeRTOS: First Steps -- A Mechanized Strategy for Safe Abstraction of CSP Specifications -- Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B -- An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model -- Towards Safe Design of Synchronous Bus Protocols in Event-B -- Mechanising Data-Types for Kernel Design in Z -- A Complete Set of Object Modeling Laws for Alloy -- Undecidability Results for Distributed Probabilistic Systems -- Formalisation and Analysis of Objects as CSP Processes -- Concolic Testing of the Multi-sector Read Operation for Flash Memory File System -- Low-Level Code Verification Based on CSP Models -- Formal Modelling of a Microcontroller Instruction Set in B -- Defining Behaviours by Quasi-finality -- Verifying Compiled File System Code -- Reasoning about General Quantum Programs over Mixed States -- A Simple and General Theoretical Account for Abstract Types. |
| Record Nr. | UNISA-996466304703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking and Artificial Intelligence [[electronic resource] ] : 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008, Revised Selected and Invited Papers / / edited by Doron A. Peled, Michael Wooldridge
| Model Checking and Artificial Intelligence [[electronic resource] ] : 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008, Revised Selected and Invited Papers / / edited by Doron A. Peled, Michael Wooldridge |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (VII, 189 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Computer programming Software engineering Computer logic Mathematical logic Artificial Intelligence Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages |
| Soggetto genere / forma | Kongress. |
| ISBN | 3-642-00431-8 |
| Classificazione |
DAT 325f
DAT 706f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verifying Time and Communication Costs of Rule-Based Reasoners -- Solving ?-Calculus Parity Games by Symbolic Planning -- Verifying Robocup Teams -- Scaling Search with Pattern Databases -- Survey on Directed Model Checking -- Automated Testing of Planning Models -- Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic -- Model Checking Driven Heuristic Search for Correct Programs -- Experimental Evaluation of a Planning Language Suitable for Formal Verification -- Relaxation Refinement: A New Method to Generate Heuristic Functions -- Model Checking Strategic Equilibria. |
| Record Nr. | UNISA-996465898003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking and Artificial Intelligence : 5th international workshop, MoChArt 2008, Patras, Greece, July 21, 2008. Revised selected and invited papers / / Doron A. Peled, Michael J. Wooldridge (eds.)
| Model Checking and Artificial Intelligence : 5th international workshop, MoChArt 2008, Patras, Greece, July 21, 2008. Revised selected and invited papers / / Doron A. Peled, Michael J. Wooldridge (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2009 |
| Descrizione fisica | 1 online resource (VII, 189 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) |
PeledDoron <1962->
WooldridgeMichael J. <1966-> |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Computer systems - Verification
Artificial intelligence |
| ISBN | 3-642-00431-8 |
| Classificazione |
DAT 325f
DAT 706f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verifying Time and Communication Costs of Rule-Based Reasoners -- Solving ?-Calculus Parity Games by Symbolic Planning -- Verifying Robocup Teams -- Scaling Search with Pattern Databases -- Survey on Directed Model Checking -- Automated Testing of Planning Models -- Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic -- Model Checking Driven Heuristic Search for Correct Programs -- Experimental Evaluation of a Planning Language Suitable for Formal Verification -- Relaxation Refinement: A New Method to Generate Heuristic Functions -- Model Checking Strategic Equilibria. |
| Record Nr. | UNINA-9910484803503321 |
| Berlin, : Springer, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model Checking Software [[electronic resource] ] : 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings / / edited by Corina S Pasareanu
| Model Checking Software [[electronic resource] ] : 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings / / edited by Corina S Pasareanu |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (X, 297 p.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming |
| ISBN | 3-642-02652-4 |
| Classificazione |
DAT 325f
SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Software Model Checking Improving Security of a Billion Computers -- On Quantitative Software Verification -- The Quest for Correctness-Beyond a Posteriori Verification -- Who Really Cares If the Program Crashes? -- Regular Papers -- Tool Presentation: Teaching Concurrency and Model Checking -- Fast, All-Purpose State Storage -- Efficient Probabilistic Model Checking on General Purpose Graphics Processors -- Improving Non-Progress Cycle Checks -- Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions -- Probabilistic Reachability for Parametric Markov Models -- Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems -- A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks -- Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation -- Symbolic Analysis via Semantic Reinterpretation -- EMMA: Explicit Model Checking Manager (Tool Presentation) -- Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution -- Subsumer-First: Steering Symbolic Reachability Analysis -- Identifying Modeling Errors in Signatures by Model Checking -- Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin -- Verification of GALS Systems by Combining Synchronous Languages and Process Calculi -- Experience with Model Checking Linearizability -- Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. |
| Record Nr. | UNISA-996465400103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model checking software : 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009 ; proceedings / / Corina S. Pasareanu (ed.)
| Model checking software : 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009 ; proceedings / / Corina S. Pasareanu (ed.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2009 |
| Descrizione fisica | 1 online resource (X, 297 p.) |
| Disciplina | 005.1 |
| Altri autori (Persone) | PasareanuCorina S |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico | Computer software - Verification |
| ISBN | 3-642-02652-4 |
| Classificazione |
DAT 325f
SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Software Model Checking Improving Security of a Billion Computers -- On Quantitative Software Verification -- The Quest for Correctness-Beyond a Posteriori Verification -- Who Really Cares If the Program Crashes? -- Regular Papers -- Tool Presentation: Teaching Concurrency and Model Checking -- Fast, All-Purpose State Storage -- Efficient Probabilistic Model Checking on General Purpose Graphics Processors -- Improving Non-Progress Cycle Checks -- Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions -- Probabilistic Reachability for Parametric Markov Models -- Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems -- A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks -- Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation -- Symbolic Analysis via Semantic Reinterpretation -- EMMA: Explicit Model Checking Manager (Tool Presentation) -- Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution -- Subsumer-First: Steering Symbolic Reachability Analysis -- Identifying Modeling Errors in Signatures by Model Checking -- Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin -- Verification of GALS Systems by Combining Synchronous Languages and Process Calculi -- Experience with Model Checking Linearizability -- Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. |
| Record Nr. | UNINA-9910484995703321 |
| Berlin ; ; New York, : Springer, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
