top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
Computers in language research [[electronic resource] ] . 2 / / edited by Walter A. Sedelow, Jr., Sally Yeates Sedelow
Computers in language research [[electronic resource] ] . 2 / / edited by Walter A. Sedelow, Jr., Sally Yeates Sedelow
Edizione [Reprint 2011]
Pubbl/distr/stampa Berlin ; ; New York, : Mouton Publishers, c1983
Descrizione fisica 1 online resource (312 p.)
Disciplina 410/.28/5
Altri autori (Persone) SedelowWalter A
SedelowSally Yeates <1931->
Collana Trends in Linguistics. Studies and Monographs [TiLSM]
Trends in linguistics.
Soggetto topico Computational linguistics
Music - Data processing
Formal languages
Formal methods (Computer science)
ISBN 3-11-082334-9
Classificazione ES 900
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto pt. 1. Formalization in literary and discourse analysis -- pt. 2. Notating the language of music and the (pause) rhythms of speech.
Record Nr. UNINA-9910785614803321
Berlin ; ; New York, : Mouton Publishers, c1983
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computers in language research [[electronic resource] ] . 2 / / edited by Walter A. Sedelow, Jr., Sally Yeates Sedelow
Computers in language research [[electronic resource] ] . 2 / / edited by Walter A. Sedelow, Jr., Sally Yeates Sedelow
Edizione [Reprint 2011]
Pubbl/distr/stampa Berlin ; ; New York, : Mouton Publishers, c1983
Descrizione fisica 1 online resource (312 p.)
Disciplina 410/.28/5
Altri autori (Persone) SedelowWalter A
SedelowSally Yeates <1931->
Collana Trends in Linguistics. Studies and Monographs [TiLSM]
Trends in linguistics.
Soggetto topico Computational linguistics
Music - Data processing
Formal languages
Formal methods (Computer science)
ISBN 3-11-082334-9
Classificazione ES 900
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto pt. 1. Formalization in literary and discourse analysis -- pt. 2. Notating the language of music and the (pause) rhythms of speech.
Record Nr. UNINA-9910824304803321
Berlin ; ; New York, : Mouton Publishers, c1983
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
CPP '16 : proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs : January 18-19, 2016, St. Petersburg, FL, USA / / edited by Jeremy Avigad and Adam Chlipala ; sponsored by ACM SIGPLAN
CPP '16 : proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs : January 18-19, 2016, St. Petersburg, FL, USA / / edited by Jeremy Avigad and Adam Chlipala ; sponsored by ACM SIGPLAN
Pubbl/distr/stampa New York : , : ACM, , 2016
Descrizione fisica 1 online resource (196 pages)
Disciplina 004.0151
Soggetto topico Computer science - Mathematics
Proof theory - Data processing
Formal methods (Computer science)
Soggetto genere / forma Electronic books.
ISBN 1-4503-4127-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Certified Programs and Proofs 2016 : proceedings of the 5th Association for Computing Machinery Special Interest Group on Programming Languages Conference on Certified Programs and Proofs : January 18-19, 2016, St. Petersburg, FL, USA
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs
Proceedings of the 5th Association for Computing Machinery Special Interest Group on Programming Languages Conference on Certified Programs and Proofs
Record Nr. UNINA-9910376541603321
New York : , : ACM, , 2016
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
CPP '17 : proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs : January 16-17, 2017, Paris, France / / edited by Yves Bertot and Viktor Vafeiadis
CPP '17 : proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs : January 16-17, 2017, Paris, France / / edited by Yves Bertot and Viktor Vafeiadis
Pubbl/distr/stampa New York : , : ACM, , 2017
Descrizione fisica 1 online resource (234 pages)
Disciplina 004.0151
Soggetto topico Computer science - Mathematics
Formal methods (Computer science)
Proof theory - Data processing
Soggetto genere / forma Electronic books.
ISBN 1-4503-4705-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Certified Programs and Proofs '17 : proceedings of the 6th Association for Computing Machinery Special Interest Group on Programming Languages Conference on Certified Programs and Proofs : January 16-17, 2017, Paris, France
Certified Programs and Proofs 2017
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Proceedings of the 6th Association for Computing Machinery Special Interest Group on Programming Languages Conference on Certified Programs and Proofs
Record Nr. UNINA-9910376430403321
New York : , : ACM, , 2017
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
CPP '18 : proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs : January 8-9, 2018, Los Angeles, CA, USA / / edited by June Andronick and Amy Felty ; sponsored by ACM SIGPLAN
CPP '18 : proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs : January 8-9, 2018, Los Angeles, CA, USA / / edited by June Andronick and Amy Felty ; sponsored by ACM SIGPLAN
Pubbl/distr/stampa New York : , : ACM, , 2018
Descrizione fisica 1 online resource (306 pages)
Disciplina 004.0151
Soggetto topico Computer science - Mathematics
Proof theory - Data processing
Formal methods (Computer science)
Soggetto genere / forma Electronic books.
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Proceedings of the seventh Association for Computing Machinery Special Interest Group on Programming Languages International Conference on Certified Programs and Proofs
Certified Programs and Proofs 2018 : proceedings of the seventh Association for Computing Machinery Special Interest Group on Programming Languages International Conference on Certified Programs and Proofs : January 8-9, 2018, Los Angeles, CA, USA
Record Nr. UNINA-9910376031103321
New York : , : ACM, , 2018
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2021]
Descrizione fisica 1 online resource (327 pages)
Disciplina 005.1
Collana Lecture notes in computer science, programming and software engineering
Soggetto topico Software engineering
Formal methods (Computer science)
ISBN 3-030-91265-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNINA-9910510561103321
Cham, Switzerland : , : Springer, , [2021]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2021]
Descrizione fisica 1 online resource (327 pages)
Disciplina 005.1
Collana Lecture notes in computer science, programming and software engineering
Soggetto topico Software engineering
Formal methods (Computer science)
ISBN 3-030-91265-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISA-996464526803316
Cham, Switzerland : , : Springer, , [2021]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Dependable software engineering : theories, tools, and applications : 8th International Symposium, SETTA 2022, Beijing, China, October 24-28, 2022, proceedings / / edited by Wei Dong, Jean-Pierre Talpin
Dependable software engineering : theories, tools, and applications : 8th International Symposium, SETTA 2022, Beijing, China, October 24-28, 2022, proceedings / / edited by Wei Dong, Jean-Pierre Talpin
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (249 pages)
Disciplina 910.5
Collana Lecture Notes in Computer Science
Soggetto topico Formal methods (Computer science)
ISBN 3-031-21213-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Preface -- Organization -- Keynotes Speakers -- On SMT Solving for Multi-threaded Program Verification -- Logic-Based Safety of Cyber-Physical Systems: Simultaneous Model Validation and Proof Transfer -- Abstraction-Based Training and Verification of Safe Deep Reinforcement Learning Systems (Extended Abstract) -- Contents -- Verification and Testing for Machine Learning -- HashC: Making DNNs' Coverage Testing Finer and Faster -- 1 Introduction -- 2 Background -- 2.1 Deep Neural Networks -- 2.2 Cryptographic Hash Function -- 2.3 Coverage Criteria -- 3 HashC Coverage Testing Framework -- 4 Evaluation -- 4.1 Experiment Design -- 4.2 Evaluation Results -- 5 Conclusion -- References -- MTUL: Towards Mutation Testing of Unsupervised Learning Systems -- 1 Introduction -- 2 Background -- 2.1 Unsupervised Learning -- 2.2 Mutation Testing -- 3 Mutation Testing Specific to Unsupervised Learning Systems -- 3.1 Mutation Testing Workflow -- 3.2 Mutation Operators -- 3.3 Mutation Scores -- 4 MUAE: The Combination of MTUL and Autoencoder -- 5 Experiment -- 5.1 Datasets -- 5.2 Research Question 1 -- 5.3 Research Question 2 -- 5.4 Research Question 3 -- 6 Related Work -- 7 Conclusion -- References -- COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking -- 1 Introduction -- 2 Core Functionality and Architecture of COOL-MC -- 3 Numerical Experiments -- 4 Conclusion and Future Work -- References -- Dependable Software Development -- VM Migration and Live-Update for Reliable Embedded Hypervisor -- 1 Introduction -- 2 Related Work -- 2.1 Embedded Hypervisor -- 2.2 Virtual Machine Migration -- 2.3 Hypervisor Update -- 3 The Design of Hypervisor -- 3.1 System Structure -- 3.2 Shared Memory -- 3.3 VM Migration -- 3.4 Hypervisor Live-Update -- 4 Evaluation -- 4.1 Environment -- 4.2 Impact on Real-Time Performance -- 4.3 Impact on Networking.
4.4 Impact on Memory -- 5 Conclusion -- References -- Mastery: Shifted-Code-Aware Structured Merging -- 1 Introduction -- 2 Preliminary -- 3 Merge Algorithm -- 3.1 Algorithm Overview -- 3.2 Top-Down Pruning Pass -- 3.3 Shifted Code Merging -- 3.4 Unordered Merging -- 3.5 Ordered Merging -- 4 Implementation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Frequency of Shifted Code (RQ1) -- 5.3 Taxonomy of Results -- 5.4 Merge Accuracy (RQ2) -- 5.5 Reported Conflicts (RQ3) -- 5.6 Runtime Performance (RQ4) -- 5.7 Discussions -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- KCL: A Declarative Language for Large-Scale Configuration and Policy Management -- 1 Introduction -- 2 Background and Related Work -- 3 Overview -- 4 Stability -- 5 Engineering -- 5.1 Structure -- 6 Scalability -- 6.1 Configuration Definition -- 6.2 Configuration Substitution -- 6.3 Configuration Merge -- 7 Workflow -- 8 Evaluation -- 8.1 Comparison with Other CLs -- 8.2 Benefits from KCL -- 9 Conclusion and Future Work -- References -- EqFix: Fixing LaTeX Equation Errors by Examples -- 1 Introduction -- 2 EqFix by Examples -- 3 Rules in EqFix -- 3.1 Error Pattern -- 3.2 Equation Pattern -- 3.3 Transformer -- 3.4 Rule Application -- 4 Rule Synthesis -- 4.1 Synthesizing Error Patterns -- 4.2 Synthesizing Transformers -- 4.3 Extension: Pattern Generalization via Lazy Relaxation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- Dependable CPS and Concurrent Systems -- Translating CPS with Shared-Variable Concurrency in SpaceEx -- 1 Introduction -- 2 Background -- 2.1 SpaceEx -- 2.2 Syntax of Our Modeling Language -- 3 Translation in SpaceEx -- 3.1 Variables -- 3.2 Discrete Behavior -- 3.3 Continous Behavior -- 3.4 Composition -- 4 Conclusion and Future Work -- References.
A Contract-Based Semantics and Refinement for Simulink -- 1 Introduction -- 2 Related Work -- 3 Syntax of Algebraic Expression of Simulink Diagrams -- 3.1 Signals -- 3.2 Blocks -- 3.3 Algebraic Expressions of Simulink Diagrams -- 4 Contract-Based Semantics of Simulink -- 5 Refinement of Simulink -- 6 Conclusion and Future Work -- References -- Decidability of Liveness for Concurrent Objects on the TSO Memory Model -- 1 Introduction -- 2 Concurrent Systems -- 2.1 Notations -- 2.2 Concurrent Objects and the Most General Client -- 2.3 TSO Operational Semantics -- 3 Liveness -- 4 Perfect/Lossy Channel Machines -- 5 Undecidability of Four Liveness Properties -- 5.1 The Lossy Channel Machine for CPCP of Abdulla et al. ch10DBLP:journalsspsiandcspsAbdullaJ96a -- 5.2 Libraries for Four Liveness Properties -- 5.3 Undecidability of Four Liveness Properties -- 6 Checking Obstruction-Freedom -- 6.1 The Basic TSO Concurrent Systems -- 6.2 Verification of Obstruction-Freedom -- 7 Conclusion -- References -- Theorem Proving and SAT -- Integration of Multiple Formal Matrix Models in Coq -- 1 Introduction -- 2 Different Formal Matrix Models -- 2.1 DepList: Dependent List -- 2.2 DepPair: Dependent Pair -- 2.3 DepRec: Dependent Record -- 2.4 NatFun: Function with Natural Indexing -- 2.5 FinFun: Function with Finite Indexing -- 3 Integrated Matrix Library -- 3.1 Mathematical Properties -- 3.2 Polymorphism and Hierarchy of Matrix Elements -- 3.3 Matrix Interface -- 3.4 Matrix Implementation -- 3.5 Conversion Between Matrix Models -- 3.6 Isomorphism of Matrix Models -- 4 Comparison of Different Matrix Models -- 5 Example of Using the Matrix Library -- 6 Conclusion -- References -- On-The-Fly Bisimilarity Checking for Fresh-Register Automata -- 1 Introduction -- 2 Background -- 3 Symbolic Reasoning -- 4 On-The-Fly Algorithms for Bisimilarity -- 4.1 Base On-the-fly Algorithm.
4.2 Generator On-the-fly Algorithm -- 5 Results -- 5.1 Benchmarks for On-the-fly Algorithms, and Existing Approaches -- 5.2 -calculus Results -- 6 Conclusions -- References -- LOGIC: A Coq Library for Logics -- 1 Introduction -- 2 Background: Coq Proof Assistant -- 3 Overview -- 4 Parameterized Definitions and Proofs -- 4.1 Connectives and Judgements -- 4.2 Proof Rules -- 4.3 Semantics and Soundness -- 4.4 Completeness -- 5 Logic Generator -- 5.1 Features of Logic Generator -- 5.2 Design of Logic Generator -- 6 Related Work -- 7 Conclusion -- A Sample Use Cases of Logic Generator -- A.1 Demo1: Intuitionistic Propositional Logic -- A.2 Demo2: A Very Small Logic -- A.3 Demo3: Intuitionistic Propositional Logic -- A.4 Demo4: Separation Logic, Without Separation Conjunction -- A.5 Demo5: Separation Logic, with Separating Conjunction -- A.6 Demo6: Separation Logic, Without Separating Implication -- A.7 Demo7: Separation Logic, Constructed from Model Level -- A.8 Mendelson's Propositional Logic -- A.9 Minimum Separation Logic -- A.10 Demo for Bedrock2's Separation Logic -- References -- Diversifying a Parallel SAT Solver with Bayesian Moment Matching -- 1 Introduction -- 2 Algorithm Description -- 3 Evaluation of slime and bmm Sequential Solvers -- 3.1 Architecture of the p-slime-bmmParallel Portfolio Solver and Results -- 4 Conclusion -- References -- Author Index.
Record Nr. UNINA-9910634038203321
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Dependable software engineering : theories, tools, and applications : 8th International Symposium, SETTA 2022, Beijing, China, October 24-28, 2022, proceedings / / edited by Wei Dong, Jean-Pierre Talpin
Dependable software engineering : theories, tools, and applications : 8th International Symposium, SETTA 2022, Beijing, China, October 24-28, 2022, proceedings / / edited by Wei Dong, Jean-Pierre Talpin
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (249 pages)
Disciplina 910.5
Collana Lecture Notes in Computer Science
Soggetto topico Formal methods (Computer science)
ISBN 3-031-21213-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Preface -- Organization -- Keynotes Speakers -- On SMT Solving for Multi-threaded Program Verification -- Logic-Based Safety of Cyber-Physical Systems: Simultaneous Model Validation and Proof Transfer -- Abstraction-Based Training and Verification of Safe Deep Reinforcement Learning Systems (Extended Abstract) -- Contents -- Verification and Testing for Machine Learning -- HashC: Making DNNs' Coverage Testing Finer and Faster -- 1 Introduction -- 2 Background -- 2.1 Deep Neural Networks -- 2.2 Cryptographic Hash Function -- 2.3 Coverage Criteria -- 3 HashC Coverage Testing Framework -- 4 Evaluation -- 4.1 Experiment Design -- 4.2 Evaluation Results -- 5 Conclusion -- References -- MTUL: Towards Mutation Testing of Unsupervised Learning Systems -- 1 Introduction -- 2 Background -- 2.1 Unsupervised Learning -- 2.2 Mutation Testing -- 3 Mutation Testing Specific to Unsupervised Learning Systems -- 3.1 Mutation Testing Workflow -- 3.2 Mutation Operators -- 3.3 Mutation Scores -- 4 MUAE: The Combination of MTUL and Autoencoder -- 5 Experiment -- 5.1 Datasets -- 5.2 Research Question 1 -- 5.3 Research Question 2 -- 5.4 Research Question 3 -- 6 Related Work -- 7 Conclusion -- References -- COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking -- 1 Introduction -- 2 Core Functionality and Architecture of COOL-MC -- 3 Numerical Experiments -- 4 Conclusion and Future Work -- References -- Dependable Software Development -- VM Migration and Live-Update for Reliable Embedded Hypervisor -- 1 Introduction -- 2 Related Work -- 2.1 Embedded Hypervisor -- 2.2 Virtual Machine Migration -- 2.3 Hypervisor Update -- 3 The Design of Hypervisor -- 3.1 System Structure -- 3.2 Shared Memory -- 3.3 VM Migration -- 3.4 Hypervisor Live-Update -- 4 Evaluation -- 4.1 Environment -- 4.2 Impact on Real-Time Performance -- 4.3 Impact on Networking.
4.4 Impact on Memory -- 5 Conclusion -- References -- Mastery: Shifted-Code-Aware Structured Merging -- 1 Introduction -- 2 Preliminary -- 3 Merge Algorithm -- 3.1 Algorithm Overview -- 3.2 Top-Down Pruning Pass -- 3.3 Shifted Code Merging -- 3.4 Unordered Merging -- 3.5 Ordered Merging -- 4 Implementation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Frequency of Shifted Code (RQ1) -- 5.3 Taxonomy of Results -- 5.4 Merge Accuracy (RQ2) -- 5.5 Reported Conflicts (RQ3) -- 5.6 Runtime Performance (RQ4) -- 5.7 Discussions -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- KCL: A Declarative Language for Large-Scale Configuration and Policy Management -- 1 Introduction -- 2 Background and Related Work -- 3 Overview -- 4 Stability -- 5 Engineering -- 5.1 Structure -- 6 Scalability -- 6.1 Configuration Definition -- 6.2 Configuration Substitution -- 6.3 Configuration Merge -- 7 Workflow -- 8 Evaluation -- 8.1 Comparison with Other CLs -- 8.2 Benefits from KCL -- 9 Conclusion and Future Work -- References -- EqFix: Fixing LaTeX Equation Errors by Examples -- 1 Introduction -- 2 EqFix by Examples -- 3 Rules in EqFix -- 3.1 Error Pattern -- 3.2 Equation Pattern -- 3.3 Transformer -- 3.4 Rule Application -- 4 Rule Synthesis -- 4.1 Synthesizing Error Patterns -- 4.2 Synthesizing Transformers -- 4.3 Extension: Pattern Generalization via Lazy Relaxation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- Dependable CPS and Concurrent Systems -- Translating CPS with Shared-Variable Concurrency in SpaceEx -- 1 Introduction -- 2 Background -- 2.1 SpaceEx -- 2.2 Syntax of Our Modeling Language -- 3 Translation in SpaceEx -- 3.1 Variables -- 3.2 Discrete Behavior -- 3.3 Continous Behavior -- 3.4 Composition -- 4 Conclusion and Future Work -- References.
A Contract-Based Semantics and Refinement for Simulink -- 1 Introduction -- 2 Related Work -- 3 Syntax of Algebraic Expression of Simulink Diagrams -- 3.1 Signals -- 3.2 Blocks -- 3.3 Algebraic Expressions of Simulink Diagrams -- 4 Contract-Based Semantics of Simulink -- 5 Refinement of Simulink -- 6 Conclusion and Future Work -- References -- Decidability of Liveness for Concurrent Objects on the TSO Memory Model -- 1 Introduction -- 2 Concurrent Systems -- 2.1 Notations -- 2.2 Concurrent Objects and the Most General Client -- 2.3 TSO Operational Semantics -- 3 Liveness -- 4 Perfect/Lossy Channel Machines -- 5 Undecidability of Four Liveness Properties -- 5.1 The Lossy Channel Machine for CPCP of Abdulla et al. ch10DBLP:journalsspsiandcspsAbdullaJ96a -- 5.2 Libraries for Four Liveness Properties -- 5.3 Undecidability of Four Liveness Properties -- 6 Checking Obstruction-Freedom -- 6.1 The Basic TSO Concurrent Systems -- 6.2 Verification of Obstruction-Freedom -- 7 Conclusion -- References -- Theorem Proving and SAT -- Integration of Multiple Formal Matrix Models in Coq -- 1 Introduction -- 2 Different Formal Matrix Models -- 2.1 DepList: Dependent List -- 2.2 DepPair: Dependent Pair -- 2.3 DepRec: Dependent Record -- 2.4 NatFun: Function with Natural Indexing -- 2.5 FinFun: Function with Finite Indexing -- 3 Integrated Matrix Library -- 3.1 Mathematical Properties -- 3.2 Polymorphism and Hierarchy of Matrix Elements -- 3.3 Matrix Interface -- 3.4 Matrix Implementation -- 3.5 Conversion Between Matrix Models -- 3.6 Isomorphism of Matrix Models -- 4 Comparison of Different Matrix Models -- 5 Example of Using the Matrix Library -- 6 Conclusion -- References -- On-The-Fly Bisimilarity Checking for Fresh-Register Automata -- 1 Introduction -- 2 Background -- 3 Symbolic Reasoning -- 4 On-The-Fly Algorithms for Bisimilarity -- 4.1 Base On-the-fly Algorithm.
4.2 Generator On-the-fly Algorithm -- 5 Results -- 5.1 Benchmarks for On-the-fly Algorithms, and Existing Approaches -- 5.2 -calculus Results -- 6 Conclusions -- References -- LOGIC: A Coq Library for Logics -- 1 Introduction -- 2 Background: Coq Proof Assistant -- 3 Overview -- 4 Parameterized Definitions and Proofs -- 4.1 Connectives and Judgements -- 4.2 Proof Rules -- 4.3 Semantics and Soundness -- 4.4 Completeness -- 5 Logic Generator -- 5.1 Features of Logic Generator -- 5.2 Design of Logic Generator -- 6 Related Work -- 7 Conclusion -- A Sample Use Cases of Logic Generator -- A.1 Demo1: Intuitionistic Propositional Logic -- A.2 Demo2: A Very Small Logic -- A.3 Demo3: Intuitionistic Propositional Logic -- A.4 Demo4: Separation Logic, Without Separation Conjunction -- A.5 Demo5: Separation Logic, with Separating Conjunction -- A.6 Demo6: Separation Logic, Without Separating Implication -- A.7 Demo7: Separation Logic, Constructed from Model Level -- A.8 Mendelson's Propositional Logic -- A.9 Minimum Separation Logic -- A.10 Demo for Bedrock2's Separation Logic -- References -- Diversifying a Parallel SAT Solver with Bayesian Moment Matching -- 1 Introduction -- 2 Algorithm Description -- 3 Evaluation of slime and bmm Sequential Solvers -- 3.1 Architecture of the p-slime-bmmParallel Portfolio Solver and Results -- 4 Conclusion -- References -- Author Index.
Record Nr. UNISA-996503470003316
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Dependable software engineering. theories, tools, and applications : 6th international symposium, setta 2020, guangzhou, china, november 24-27, 2020, proceedings / / edited by Jun Pang, Lijun Zhang
Dependable software engineering. theories, tools, and applications : 6th international symposium, setta 2020, guangzhou, china, november 24-27, 2020, proceedings / / edited by Jun Pang, Lijun Zhang
Edizione [1st ed. 2020.]
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2020]
Descrizione fisica 1 online resource (XIII, 203 p. 228 illus., 31 illus. in color.)
Disciplina 005.1
Collana Programming and Software Engineering
Soggetto topico Formal methods (Computer science)
Computers
Software engineering
ISBN 3-030-62822-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto The Road Ahead for Supervisor Synthesis -- Reentrancy? Yes. Reentrancy bug? No -- Graph Transformation Systems: a Semantics Based on (Stochastic) Symmetric Nets -- Modelling and Implementation of Unmanned Aircraft Collision Avoidance -- Randomized Re nement Checking of Timed I/O Automata -- Computing Linear Arithmetic Representation for Reachability Relation of One-counter Automata -- Compiling FL^{res} on Finite Words -- Symbolic Model Checking with Sentential Decision Diagrams -- Probably Approximately Correct Interpolants Generation -- Symbolic Verification of MPI Programs with Non-deterministic Synchronizations -- Learning Safe Neural Network Controllers with Barrier Certificates -- Software Defect-proneness Prediction Based on Package Cohesion and Coupling Metrics.
Record Nr. UNINA-9910427673603321
Cham, Switzerland : , : Springer, , [2020]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui