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.) |
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 Techniques in Real-Time and Fault-Tolerant Systems [[electronic resource] ] : 5th International Symposium, FTRTFT'98, Lyngby, Denmark, September 14-18, 1998, Proceedings / / edited by Anders P. Ravn, Hans Rischel |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (IX, 347 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Architecture, Computer Computers Computer logic Microprocessors Special purpose computers Programming Languages, Compilers, Interpreters Computer System Implementation Theory of Computation Logics and Meanings of Programs Processor Architectures Special Purpose and Application-Based Systems |
ISBN | 3-540-49792-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Challenges in the utilization of formal methods -- On the need for practical formal methods -- A general framework for the composition of timed systems -- Operational and logical semantics for polling real-time systems -- A finite-domain semantics for testing temporal logic specifications -- Duration Calculus of Weakly Monotonic Time -- Reuse in requirements engineering: Discovery and application of a real-time requirement pattern -- A modular visual model for hybrid systems -- Integrating real-time structured design and formal techniques -- Duration Calculus in the specification of safety requirements -- Automated stream-based analysis of fault-tolerance -- Designing a provably correct robt control system using a ‘lean’ formal method -- Static analysis to identify invariants in RSML specifications -- Partition refinement in real-time model checking -- Formal verification of stabilizing systems -- Synchronizing clocked transition systems -- Some decidability results for duration calculus under synchronous interpretation -- Fair synchronous transition systems and their liveness proofs -- Dynamical properties of timed automata -- An algorithm for the approximative analysis of rectangular automata -- On checking parallel real-time systems for linear duration properties -- A practical and complete algorithm for testing real-time systems -- Mechanical verification of clock synchronization algorithms -- Compiling graphical real-time specifications into silicon -- Towards a formal semantics of verilog using duration calculus -- The ICOS synthesis environment -- Kronos: A model-checking tool for real-time systems -- SGLOT: A visual tool for structural LOTOS specifications -- Discrete-time Promela and Spin -- Moby/PLC — Graphical development of PLC-automata -- Predictability in critical systems. |
Record Nr. | UNISA-996466151803316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Techniques in Real-Time and Fault-Tolerant Systems [[electronic resource] ] : 5th International Symposium, FTRTFT'98, Lyngby, Denmark, September 14-18, 1998, Proceedings / / edited by Anders P. Ravn, Hans Rischel |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (IX, 347 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Architecture, Computer Computers Computer logic Microprocessors Special purpose computers Programming Languages, Compilers, Interpreters Computer System Implementation Theory of Computation Logics and Meanings of Programs Processor Architectures Special Purpose and Application-Based Systems |
ISBN | 3-540-49792-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Challenges in the utilization of formal methods -- On the need for practical formal methods -- A general framework for the composition of timed systems -- Operational and logical semantics for polling real-time systems -- A finite-domain semantics for testing temporal logic specifications -- Duration Calculus of Weakly Monotonic Time -- Reuse in requirements engineering: Discovery and application of a real-time requirement pattern -- A modular visual model for hybrid systems -- Integrating real-time structured design and formal techniques -- Duration Calculus in the specification of safety requirements -- Automated stream-based analysis of fault-tolerance -- Designing a provably correct robt control system using a ‘lean’ formal method -- Static analysis to identify invariants in RSML specifications -- Partition refinement in real-time model checking -- Formal verification of stabilizing systems -- Synchronizing clocked transition systems -- Some decidability results for duration calculus under synchronous interpretation -- Fair synchronous transition systems and their liveness proofs -- Dynamical properties of timed automata -- An algorithm for the approximative analysis of rectangular automata -- On checking parallel real-time systems for linear duration properties -- A practical and complete algorithm for testing real-time systems -- Mechanical verification of clock synchronization algorithms -- Compiling graphical real-time specifications into silicon -- Towards a formal semantics of verilog using duration calculus -- The ICOS synthesis environment -- Kronos: A model-checking tool for real-time systems -- SGLOT: A visual tool for structural LOTOS specifications -- Discrete-time Promela and Spin -- Moby/PLC — Graphical development of PLC-automata -- Predictability in critical systems. |
Record Nr. | UNINA-9910767565803321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Hybrid Systems [[electronic resource] /] / edited by Robert L. Grossman, Anil Nerode, Anders P. Ravn, Hans Rischel |
Edizione | [1st ed. 1993.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 |
Descrizione fisica | 1 online resource (VIII, 476 p.) |
Disciplina | 004.1/9 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Microprocessors
Control engineering Computers Special purpose computers Software engineering Processor Architectures Control and Systems Theory Theory of Computation Special Purpose and Application-Based Systems Software Engineering Computation by Abstract Devices |
ISBN | 3-540-48060-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Verifying hybrid systems -- An extended duration calculus for hybrid real-time systems -- Towards refining temporal specifications into hybrid systems -- Hybrid systems in TLA+ -- Hybrid models with fairness and distributed clocks -- A compositional approach to the design of hybrid systems -- An approach to the description and analysis of hybrid systems -- Integration Graphs: A class of decidable hybrid systems -- Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems -- Hybrid Systems: the SIGNAL approach -- A dynamical simulation facility for hybrid systems -- Event identification and intelligent hybrid control -- Multiple agent hybrid control architecture -- Models for hybrid systems: Automata, topologies, controllability, observability -- Some remarks about flows in hybrid systems -- Hybrid system modeling and autonomous control systems -- Fault accommodation in feedback control systems -- On formal support for industrial-scale requirements analysis -- A formal approach to computer systems requirements documentation. |
Record Nr. | UNISA-996466047303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
JTRES 2011 : proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, September 26-28, 2011, University of York, Kings Manor, York, United Kingdom |
Autore | Ravn Anders P |
Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2011 |
Descrizione fisica | 1 online resource (135 pages) |
Altri autori (Persone) |
RavnAnders P
WellingsAndrew J |
Collana | ACM Other conferences |
Soggetto topico |
Engineering & Applied Sciences
Computer Science |
ISBN | 1-4503-0731-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Altri titoli varianti |
Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems
JTRES '11 the 9th International Workshop on Java Technologies for Real-time and Embedded Systems, York, United Kingdom - September 26-28, 2011 |
Record Nr. | UNINA-9910376505503321 |
Ravn Anders P | ||
[Place of publication not identified], : ACM, 2011 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|