Formal methods for industrial critical systems / / volume editors, Maria Alpuente, Byron Cooker, Christophe Joubert |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin ; ; London, : Springer, c2009 |
Descrizione fisica | 1 online resource (X, 213 p.) |
Disciplina | 005.131 |
Altri autori (Persone) |
AlpuenteMaria
CookByron JoubertChristophe |
Collana | Lecture notes in computer science |
Soggetto topico |
Computer programs - Verification
Formal methods (Computer science) Software engineering |
ISBN | 3-642-04570-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Attacking Large Industrial Code with Bi-abductive Inference -- On a Uniform Framework for the Definition of Stochastic Process Languages -- Applying a Formal Method in Industry: A 15-Year Trajectory -- What’s in Common between Test, Model Checking, and Decision Procedures? -- Contributed Papers -- Verifying Cryptographic Software Correctness with Respect to Reference Implementations -- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software -- Dynamic State Space Partitioning for External Memory Model Checking -- Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle -- Modeling Concurrent Systems with Shared Resources -- Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs -- Formal Analysis of Non-determinism in Verilog Cell Library Simulation Models -- Preemption Abstraction -- A Rigorous Methodology for Composing Services -- A Certified Implementation on Top of the Java Virtual Machine -- Selected Posters -- Formal Development for Railway Signaling Using Commercial Tools -- Integrated Formal Approach for Qualified Critical Embedded Code Generator -- Visualising Event-B Models with B-Motion Studio -- Behavioural Analysis of an I2C Linux Driver -- Model-Based Testing of Electronic Passports -- Developing a Decision Support Tool for Dam Management with SPIN. |
Record Nr. | UNINA-9910484030903321 |
Berlin ; ; London, : Springer, c2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Static analysis : 15th international symposium, SAS 2008, Valencia, Spain, July 16-18, 2008 : proceedings / / Maria Alpuente, German Vidal (eds.) |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2008 |
Descrizione fisica | 1 online resource (X, 379 p.) |
Disciplina | 005.1 |
Altri autori (Persone) |
AlpuenteMaria
VidalGerman (German Francisco Vidal Oriola) |
Collana |
Lecture notes in computer science
LNCS sublibrary. SL 2, Programming and software engineering |
Soggetto topico |
Computer programming
Programming languages (Electronic computers) |
ISBN | 3-540-69166-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Transforming Abstract Interpretations by Abstract Interpretation -- Reflections on the Role of Static Analysis in Cooperative Bug Isolation -- Contributed Papers -- Relational Analysis of Correlation -- Convex Hull of Arithmetic Automata -- Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors -- Protocol Inference Using Static Path Profiles -- Solving Multiple Dataflow Queries Using WPDSs -- Field Flow Sensitive Pointer and Escape Analysis for Java Using Heap Array SSA -- Typing Linear Constraints for Moding CLP( ) Programs -- On Polymorphic Recursion, Type Systems, and Abstract Interpretation -- Modal Abstractions of Concurrent Behaviour -- Hiding Software Watermarks in Loop Structures -- Inferring Min and Max Invariants Using Max-Plus Polyhedra -- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors -- Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis -- SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement -- Flow Analysis, Linearity, and PTIME -- Quantum Entanglement Analysis Based on Abstract Interpretation -- Language Strength Reduction -- Analysing All Polynomial Equations in -- Splitting the Control Flow with Boolean Flags -- Reasoning about Control Flow in the Presence of Transient Faults -- A Calculational Approach to Control-Flow Analysis by Abstract Interpretation -- Heap Decomposition for Concurrent Shape Analysis. |
Altri titoli varianti | SAS 2008 |
Record Nr. | UNINA-9910483165003321 |
Berlin ; ; New York, : Springer, c2008 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|