Critical Systems: Formal Methods and Automated Verification [[electronic resource] ] : Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings / / edited by Laure Petrucci, Cristina Seceleanu, Ana Cavalcanti |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XIV, 235 p. 52 illus.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Programming languages (Electronic computers)
Computer logic Software engineering Special purpose computers Mathematical logic Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Software Engineering Special Purpose and Application-Based Systems Mathematical Logic and Formal Languages |
ISBN | 3-319-67113-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Automated verification techniques -- Testing and scheduling -- Formal Methods for mobile and autonomous robots -- Modeling and analysis techniques. |
Record Nr. | UNISA-996465913403316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Critical Systems: Formal Methods and Automated Verification [[electronic resource] ] : Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings / / edited by Laure Petrucci, Cristina Seceleanu, Ana Cavalcanti |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XIV, 235 p. 52 illus.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Programming languages (Electronic computers)
Computer logic Software engineering Special purpose computers Mathematical logic Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Software Engineering Special Purpose and Application-Based Systems Mathematical Logic and Formal Languages |
ISBN | 3-319-67113-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Automated verification techniques -- Testing and scheduling -- Formal Methods for mobile and autonomous robots -- Modeling and analysis techniques. |
Record Nr. | UNINA-9910484112003321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
FM 2009: Formal Methods [[electronic resource] ] : Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings / / edited by Ana Cavalcanti, Dennis Dams |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (XVII, 820 p.) |
Disciplina | 005.1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
User interfaces (Computer systems) Computer logic Programming languages (Electronic computers) Computer programming Software Engineering Software Engineering/Programming and Operating Systems User Interfaces and Human Computer Interaction Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Programming Techniques |
Soggetto genere / forma |
Eindhoven (2009)
Kongress. |
ISBN | 3-642-05089-1 |
Classificazione |
DAT 310f
DAT 510f SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Formal Methods for Privacy -- What Can Formal Methods Bring to Systems Biology? -- Guess and Verify – Back to the Future -- Verification, Testing and Statistics -- Security, Probability and Nearly Fair Coins in the Cryptographers’ Café -- Model Checking I -- Recursive Abstractions for Parameterized Systems -- Abstract Model Checking without Computing the Abstraction -- Three-Valued Spotlight Abstractions -- Fair Model Checking with Process Counter Abstraction -- Compositionality -- Systematic Development of Trustworthy Component Systems -- Partial Order Reductions Using Compositional Confluence Detection -- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition -- Verification -- Abstract Specification of the UBIFS File System for Flash Memory -- Inferring Mealy Machines -- Formal Management of CAD/CAM Processes -- Concurrency -- Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way -- Symbolic Predictive Analysis for Concurrent Programs -- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study -- Refinement -- Sums and Lovers: Case Studies in Security, Compositionality and Refinement -- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing -- Model Checking Linearizability via Refinement -- Static Analysis -- It’s Doomed; We Can Prove It -- “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis -- Field-Sensitive Value Analysis by Field-Insensitive Analysis -- Theorem Proving -- Making Temporal Logic Calculational: A Tool for Unification and Discovery -- A Tableau for CTL* -- Certifiable Specification and Verification of C Programs -- Formal Reasoning about Expectation Properties for Continuous Random Variables -- Semantics -- The Denotational Semantics of slotted-Circus -- Unifying Probability with Nondeterminism -- Towards an Operational Semantics for Alloy -- A Robust Semantics Hides Fewer Errors -- Special Track: Industrial Applications I -- Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks -- Formal Verification of Avionics Software Products -- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study -- Object-Orientation -- Connecting UML and VDM++ with Open Tool Support -- Language and Tool Support for Class and State Machine Refinement in UML-B -- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects -- Abstract Object Creation in Dynamic Logic -- Pointers -- Reasoning about Memory Layouts -- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis -- Real-Time -- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery -- Verifying Real-Time Systems against Scenario-Based Requirements -- Special Track: Tools and Industrial Applications II -- Formal Specification of a Cardiac Pacing System -- Automated Property Verification for Large Scale B Models -- Reduced Execution Semantics of MPI: From Theory to Practice -- Model Checking II -- A Metric Encoding for Bounded Model Checking -- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method -- Verifying Information Flow Control over Unbounded Processes -- Specification and Verification of Web Applications in Rewriting Logic -- Industry-Day Abstracts -- Verifying the Microsoft Hyper-V Hypervisor with VCC -- Industrial Practice in Formal Methods: A Review -- Model-Based GUI Testing Using Uppaal at Novo Nordisk. |
Record Nr. | UNINA-9910483872003321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
FM 2009: Formal Methods [[electronic resource] ] : Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings / / edited by Ana Cavalcanti, Dennis Dams |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (XVII, 820 p.) |
Disciplina | 005.1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
User interfaces (Computer systems) Computer logic Programming languages (Electronic computers) Computer programming Software Engineering Software Engineering/Programming and Operating Systems User Interfaces and Human Computer Interaction Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Programming Techniques |
Soggetto genere / forma |
Eindhoven (2009)
Kongress. |
ISBN | 3-642-05089-1 |
Classificazione |
DAT 310f
DAT 510f SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Formal Methods for Privacy -- What Can Formal Methods Bring to Systems Biology? -- Guess and Verify – Back to the Future -- Verification, Testing and Statistics -- Security, Probability and Nearly Fair Coins in the Cryptographers’ Café -- Model Checking I -- Recursive Abstractions for Parameterized Systems -- Abstract Model Checking without Computing the Abstraction -- Three-Valued Spotlight Abstractions -- Fair Model Checking with Process Counter Abstraction -- Compositionality -- Systematic Development of Trustworthy Component Systems -- Partial Order Reductions Using Compositional Confluence Detection -- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition -- Verification -- Abstract Specification of the UBIFS File System for Flash Memory -- Inferring Mealy Machines -- Formal Management of CAD/CAM Processes -- Concurrency -- Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way -- Symbolic Predictive Analysis for Concurrent Programs -- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study -- Refinement -- Sums and Lovers: Case Studies in Security, Compositionality and Refinement -- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing -- Model Checking Linearizability via Refinement -- Static Analysis -- It’s Doomed; We Can Prove It -- “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis -- Field-Sensitive Value Analysis by Field-Insensitive Analysis -- Theorem Proving -- Making Temporal Logic Calculational: A Tool for Unification and Discovery -- A Tableau for CTL* -- Certifiable Specification and Verification of C Programs -- Formal Reasoning about Expectation Properties for Continuous Random Variables -- Semantics -- The Denotational Semantics of slotted-Circus -- Unifying Probability with Nondeterminism -- Towards an Operational Semantics for Alloy -- A Robust Semantics Hides Fewer Errors -- Special Track: Industrial Applications I -- Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks -- Formal Verification of Avionics Software Products -- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study -- Object-Orientation -- Connecting UML and VDM++ with Open Tool Support -- Language and Tool Support for Class and State Machine Refinement in UML-B -- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects -- Abstract Object Creation in Dynamic Logic -- Pointers -- Reasoning about Memory Layouts -- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis -- Real-Time -- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery -- Verifying Real-Time Systems against Scenario-Based Requirements -- Special Track: Tools and Industrial Applications II -- Formal Specification of a Cardiac Pacing System -- Automated Property Verification for Large Scale B Models -- Reduced Execution Semantics of MPI: From Theory to Practice -- Model Checking II -- A Metric Encoding for Bounded Model Checking -- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method -- Verifying Information Flow Control over Unbounded Processes -- Specification and Verification of Web Applications in Rewriting Logic -- Industry-Day Abstracts -- Verifying the Microsoft Hyper-V Hypervisor with VCC -- Industrial Practice in Formal Methods: A Review -- Model-Based GUI Testing Using Uppaal at Novo Nordisk. |
Record Nr. | UNISA-996466367603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods and Software Engineering [[electronic resource] ] : 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009, Proceedings / / edited by Karin Breitman, Ana Cavalcanti |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (XIV, 758 p.) |
Disciplina | 004n/a |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer programming Computers Mathematical logic Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Models and Principles Mathematical Logic and Formal Languages |
Soggetto genere / forma |
Kongress.
Rio de Janeiro (2009) |
ISBN | 3-642-10373-1 |
Classificazione |
DAT 310f
DAT 510f SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Seamless Model Driven Systems Engineering Based on Formal Models -- Compositional Verification of Input-Output Conformance via CSP Refinement Checking -- Testing I -- Symbolic Query Exploration -- Event Listener Analysis and Symbolic Execution for Testing GUI Applications -- An Empirical Study of Structural Constraint Solving Techniques -- Protocols -- Improving Automatic Verification of Security Protocols with XOR -- Modeling and Verification of Privacy Enhancing Protocols -- Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support -- Testing II -- Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing -- A Statistical Approach to Test Stochastic and Probabilistic Systems -- Qualitative Action Systems -- Verification -- RAFFS: Model Checking a Robust Abstract Flash File Store -- European Train Control System: A Case Study in Formal Verification -- Development of Security Software: A High Assurance Methodology -- Model Checking I -- Bounded Semantics of CTL and SAT-Based Verification -- Graded-CTL: Satisfiability and Symbolic Model Checking -- Approximate Model Checking of PCTL Involving Unbounded Path Properties -- Object-Orientation -- A Graph-Based Operational Semantics of OO Programs -- Modeling and Analysis of Thread-Pools in an Industrial Communication Platform -- A Verification System for Distributed Objects with Asynchronous Method Calls -- Model checking II -- A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties -- Scalable Multi-core Model Checking Fairness Enhanced Systems -- Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language -- Event-B -- Supporting Reuse of Event-B Developments through Generic Instantiation -- A Lazy Unbounded Model Checker for Event-B -- Proof Assisted Model Checking for B -- Compilation -- Machine-Checked Sequencer for Critical Embedded Code Generator -- Implementing a Direct Method for Certificate Translation -- Process Algebra -- Algorithmic Verification with Multiple and Nested Parameters -- Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction -- Refinement -- Modal Systems: Specification, Refinement and Realisation -- Refinement-Preserving Co-evolution -- Algebraic Specifications -- Circular Coinduction with Special Contexts -- The VSE Refinement Method in Hets -- Real-Time Systems -- A Compositional Approach on Modal Specifications for Timed Systems -- An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata -- Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude -- Specifying and Verifying Business Processes Using PPML. |
Record Nr. | UNISA-996466305903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods and Software Engineering [[electronic resource] ] : 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009, Proceedings / / edited by Karin Breitman, Ana Cavalcanti |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (XIV, 758 p.) |
Disciplina | 004n/a |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer programming Computers Mathematical logic Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Models and Principles Mathematical Logic and Formal Languages |
Soggetto genere / forma |
Kongress.
Rio de Janeiro (2009) |
ISBN | 3-642-10373-1 |
Classificazione |
DAT 310f
DAT 510f SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Seamless Model Driven Systems Engineering Based on Formal Models -- Compositional Verification of Input-Output Conformance via CSP Refinement Checking -- Testing I -- Symbolic Query Exploration -- Event Listener Analysis and Symbolic Execution for Testing GUI Applications -- An Empirical Study of Structural Constraint Solving Techniques -- Protocols -- Improving Automatic Verification of Security Protocols with XOR -- Modeling and Verification of Privacy Enhancing Protocols -- Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support -- Testing II -- Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing -- A Statistical Approach to Test Stochastic and Probabilistic Systems -- Qualitative Action Systems -- Verification -- RAFFS: Model Checking a Robust Abstract Flash File Store -- European Train Control System: A Case Study in Formal Verification -- Development of Security Software: A High Assurance Methodology -- Model Checking I -- Bounded Semantics of CTL and SAT-Based Verification -- Graded-CTL: Satisfiability and Symbolic Model Checking -- Approximate Model Checking of PCTL Involving Unbounded Path Properties -- Object-Orientation -- A Graph-Based Operational Semantics of OO Programs -- Modeling and Analysis of Thread-Pools in an Industrial Communication Platform -- A Verification System for Distributed Objects with Asynchronous Method Calls -- Model checking II -- A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties -- Scalable Multi-core Model Checking Fairness Enhanced Systems -- Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language -- Event-B -- Supporting Reuse of Event-B Developments through Generic Instantiation -- A Lazy Unbounded Model Checker for Event-B -- Proof Assisted Model Checking for B -- Compilation -- Machine-Checked Sequencer for Critical Embedded Code Generator -- Implementing a Direct Method for Certificate Translation -- Process Algebra -- Algorithmic Verification with Multiple and Nested Parameters -- Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction -- Refinement -- Modal Systems: Specification, Refinement and Realisation -- Refinement-Preserving Co-evolution -- Algebraic Specifications -- Circular Coinduction with Special Contexts -- The VSE Refinement Method in Hets -- Real-Time Systems -- A Compositional Approach on Modal Specifications for Timed Systems -- An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata -- Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude -- Specifying and Verifying Business Processes Using PPML. |
Record Nr. | UNINA-9910483945003321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Fundamental Approaches to Software Engineering : 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings / / edited by Dirk Beyer, Ana Cavalcanti |
Autore | Beyer Dirk |
Edizione | [1st ed. 2024.] |
Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
Descrizione fisica | 1 online resource (346 pages) |
Disciplina | 005.1 |
Altri autori (Persone) | CavalcantiAna |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Operating systems (Computers) Computer science Microprogramming Computer systems Natural language processing (Computer science) Software Engineering Operating Systems Theory of Computation Control Structures and Microprogramming Computer System Implementation Natural Language Processing (NLP) |
ISBN | 3-031-57259-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | From Mechanized Semantics to Verified Compilation: The Clight Semantics of CompCert -- Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models -- Probabilistic Runtime Enforcement of Executable BPMN Processes -- Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems -- Formal Specification of Trusted Execution Environment APIs -- Monitoring the Future of Smart Contracts -- Comprehending Object State via Dynamic Class Invariant Learning -- Detection for Large-Scale Online Service Systems Using Multi-Channel Data -- Refinement Verification of OS Services based on a Verified Preemptive Microkernel -- Fuzzy quantitative attack tree analysis -- Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation -- Invariant-based Program Repair -- Can ChatGPT support software verification -- Combining Deductive Verification with Shape Analysis -- First Steps towards Deductive Verification of LLVM IR -- FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution) -- Fizzer: New Gray-Box Fuzzer (Competition Contribution) -- KLEEF: Symbolic Execution Engine (Competition Contribution) -- TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation (Competition Contribution) -- Ultimate TestGen: Test Case Generation with Automata-based Software Model Checking (Competition Contribution). |
Record Nr. | UNISA-996594169903316 |
Beyer Dirk | ||
Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Fundamental Approaches to Software Engineering : 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings / / edited by Dirk Beyer, Ana Cavalcanti |
Autore | Beyer Dirk |
Edizione | [1st ed. 2024.] |
Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
Descrizione fisica | 1 online resource (346 pages) |
Disciplina | 005.1 |
Altri autori (Persone) | CavalcantiAna |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Operating systems (Computers) Computer science Microprogramming Computer systems Natural language processing (Computer science) Software Engineering Operating Systems Theory of Computation Control Structures and Microprogramming Computer System Implementation Natural Language Processing (NLP) |
ISBN | 3-031-57259-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | From Mechanized Semantics to Verified Compilation: The Clight Semantics of CompCert -- Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models -- Probabilistic Runtime Enforcement of Executable BPMN Processes -- Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems -- Formal Specification of Trusted Execution Environment APIs -- Monitoring the Future of Smart Contracts -- Comprehending Object State via Dynamic Class Invariant Learning -- Detection for Large-Scale Online Service Systems Using Multi-Channel Data -- Refinement Verification of OS Services based on a Verified Preemptive Microkernel -- Fuzzy quantitative attack tree analysis -- Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation -- Invariant-based Program Repair -- Can ChatGPT support software verification -- Combining Deductive Verification with Shape Analysis -- First Steps towards Deductive Verification of LLVM IR -- FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution) -- Fizzer: New Gray-Box Fuzzer (Competition Contribution) -- KLEEF: Symbolic Execution Engine (Competition Contribution) -- TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation (Competition Contribution) -- Ultimate TestGen: Test Case Generation with Automata-based Software Model Checking (Competition Contribution). |
Record Nr. | UNINA-9910847393203321 |
Beyer Dirk | ||
Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Refinement Techniques in Software Engineering [[electronic resource] ] : First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures / / edited by Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
Edizione | [1st ed. 2006.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
Descrizione fisica | 1 online resource (XI, 393 p.) |
Disciplina | 005.1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Management information systems Computer science Software Engineering/Programming and Operating Systems Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Management of Computing and Information Systems |
ISBN | 3-540-46254-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Refinement: An overview -- Transformation Laws for Sequential Object-Oriented Programming -- Using CSP -- Developing and Reasoning About Probabilistic Programs in pGCL -- Real-Time and Fault-Tolerant Systems -- A Tutorial Introduction to CSP in Unifying Theories of Programming -- Using the Compliance Notation in Industry -- Techniques for Temporal Logic Model Checking. |
Record Nr. | UNISA-996466070703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Refinement Techniques in Software Engineering [[electronic resource] ] : First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures / / edited by Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
Edizione | [1st ed. 2006.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
Descrizione fisica | 1 online resource (XI, 393 p.) |
Disciplina | 005.1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Management information systems Computer science Software Engineering/Programming and Operating Systems Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Management of Computing and Information Systems |
ISBN | 3-540-46254-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Refinement: An overview -- Transformation Laws for Sequential Object-Oriented Programming -- Using CSP -- Developing and Reasoning About Probabilistic Programs in pGCL -- Real-Time and Fault-Tolerant Systems -- A Tutorial Introduction to CSP in Unifying Theories of Programming -- Using the Compliance Notation in Industry -- Techniques for Temporal Logic Model Checking. |
Record Nr. | UNINA-9910484097803321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|