MARC details
| 000 -LEADER |
|---|
| fixed length control field |
05924cam a2200649 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
on1352973612 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250707094744.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS |
|---|
| fixed length control field |
m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr un|---aucuu |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
221203s2023 sz o 101 0 eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
EBLCP |
| Language of cataloging |
eng |
| Transcribing agency |
EBLCP |
| Modifying agency |
GW5XE |
| -- |
YDX |
| -- |
OCLCF |
| -- |
OCLCO |
| -- |
WSU |
| -- |
OCLCO |
| 019 ## - |
|---|
| -- |
1352795144 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783031224768 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3031224760 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
3031224752 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9783031224751 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/978-3-031-22476-8 |
| Source of number or code |
doi |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
AU@ |
| System control number |
000073032325 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)1352973612 |
| Canceled/invalid control number |
(OCoLC)1352795144 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.758 |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
UMZ |
| Source |
bicssc |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
COM051230 |
| Source |
bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
UMZ |
| Source |
thema |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
004.01/51 |
| Edition number |
23/eng/20221208 |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
Brazilian Symposium on Formal Methods |
| Number of part/section/meeting |
(25th : |
| Date of meeting |
2022 : |
| Location of meeting |
Online) |
| 9 (RLIN) |
977482 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Formal methods : |
| Remainder of title |
25th Brazilian Symposium, SBMF 2022, Virtual event, December 6-9, 2022, Proceedings / |
| Statement of responsibility, etc. |
Lucas Lima, Vince Molnár (eds.). |
| 246 3# - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
SBMF 2022 |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Cham : |
| Name of publisher, distributor, etc. |
Springer, |
| Date of publication, distribution, etc. |
2023. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (154 p.). |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture Notes in Computer Science ; |
| Volume/sequential designation |
13768 |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Intro -- Preface -- Organization -- Invited Talks -- Cooperative Verification -- Taming Monsters with Dragons: A Fractal Approach to Digital Twin Pipelines -- Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community -- Some Applications of Formal Methods -- Contents -- Model Checking and Semantics -- An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata -- 1 Introduction -- 2 Timed automata -- 3 The Class TADS -- 4 The Notion of Optimality -- 5 Finding an Optimal Allocation of Clocks |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
5.1 Liveness Analysis of Clocks -- 5.2 Clock Allocation -- 5.3 The Clock Allocation Algorithm -- 5.4 Generating Clock Constraints and Clock Resets -- 6 Related Work and Conclusions -- References -- Formalization of Functional Block Diagrams Using HOL Theorem Proving -- 1 Introduction -- 2 Preliminaries -- 2.1 Formal ET Modeling -- 2.2 Formal ET Probabilistic Analysis -- 3 Functional Block Diagrams -- 4 FBD Formalization -- 4.1 Formal FBD Modeling -- 4.2 Formal FBD Probabilistic Analysis -- 5 Conclusions -- References -- Generation and Synthesis |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching -- 1 Introduction -- 2 Basic Definitions -- 3 Expansion and Transformation -- 3.1 Unrolling -- 3.2 Recursion Elimination -- 4 Term Generation -- 4.1 Soundness of Term Generation -- 5 Quick-Checking Properties -- 6 Related Work -- 7 Conclusion -- References -- Automatic Generation of Verified Concurrent Hardware Using VHDL -- 1 Introduction -- 1.1 Related Work -- 2 Theoretical Background -- 2.1 CSP -- 2.2 VHDL -- 3 CSP to VHDL Translation -- 3.1 Translation Overview -- 3.2 Restrictions -- 4 Tool Support |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
5 Case Study -- 6 Conclusion -- References -- Synthesis of Implementations for Divide-and-Conquer Specifications -- 1 Introduction -- 2 Preliminaries -- 3 From Divide-and-Conquer Specifications to Their Implementations -- 3.1 The Synthesis Rule -- 4 Case Study: Deriving an Implementation of a Greedy Algorithm -- 4.1 Weighted Matroids and Their Bases -- 4.2 Establishing max-basisI as a Divide-and-Conquer Specification -- 4.3 Implementations of Decomposition and Composition -- 5 Related Work -- 6 Conclusions and Outlook -- A The Three Auxiliary Lemmas -- References -- Verification and Solvers |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover -- 1 Introduction -- 2 Background -- 2.1 Block Diagrams and MDD -- 2.2 Running Example -- Simple Actuator System (SAS) -- 2.3 Formal Verification and CSP -- 2.4 tock-CSP -- 2.5 Roscoe and Dathi's Compositional Deadlock Analysis Theory -- 2.6 CSP-Prover -- 3 Mechanised Compositional Verification of Timed Process Networks -- 3.1 Time-Stop Free Processes -- 3.2 Time-Stop Free Process Networks -- 3.3 Mechanisation in CSP-Prover -- 4 From Simulink to tock-CSP -- 5 Conclusion and Future Works -- References |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Excommunication: Transforming -Calculus Specifications to Remove Internal Communication |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
This book constitutes the refereed proceedings of the 25th Brazilian Symposium on Formal Methods, SBMF 2022, which was held virtually in December 2022. The 8 regular papers presented in this book were carefully reviewed and selected from 15 submissions. The symposium focuses on the development, dissemination, and use of formal methods for the construction of high-quality computational systems, aiming to promote opportunities for researchers and practitioners with an interest in formal methods to discuss the recent advances in this area. . |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Includes author index. |
| 588 0# - SOURCE OF DESCRIPTION NOTE |
|---|
| Source of description note |
Online resource; title from PDF title page (SpringerLink, viewed December 8, 2022). |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Formal methods (Computer science) |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
15679 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Méthodes formelles (Informatique) |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
18838 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Formal methods (Computer science) |
| Source of heading or term |
fast |
| 9 (RLIN) |
15635 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
proceedings (reports) |
| Source of term |
aat |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings |
| Source of term |
fast |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings. |
| Source of term |
lcgft |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Actes de congrès. |
| Source of term |
rvmgf |
| 9 (RLIN) |
609890 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Lima, Lucas. |
| 9 (RLIN) |
977483 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Molnár, Vince. |
| 9 (RLIN) |
977484 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Main entry heading |
Lima, Lucas |
| Title |
Formal Methods: Foundations and Applications |
| Place, publisher, and date of publication |
Cham : Springer International Publishing AG,c2023 |
| International Standard Book Number |
9783031224751 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
13768. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
<a href="https://link.springer.com/10.1007/978-3-031-22476-8">https://link.springer.com/10.1007/978-3-031-22476-8</a> |
| 938 ## - |
|---|
| -- |
ProQuest Ebook Central |
| -- |
EBLB |
| -- |
EBL7150675 |
| 938 ## - |
|---|
| -- |
YBP Library Services |
| -- |
YANK |
| -- |
18240331 |
| 994 ## - |
|---|
| -- |
92 |
| -- |
ATIST |