Formal methods [electronic resource] : 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings / Gustavo Carvalho, Volker Stolz (eds.)
This book constitutes the refereed proceedings of the 23rd Brazilian Symposium on Formal Methods, SBMF 2020, which was supposed to take place in Ouro Preto, Brazil, in November 2020. Instead the symposium took place virtually due to the COVID-19 pandemic. The 10 regular papers presented together wit...
Saved in:
| Online Access: |
Full Text (via Springer) |
|---|---|
| Corporate Author: | |
| Other Authors: | , |
| Other title: | SBMF 2020. |
| Format: | Electronic Conference Proceeding eBook |
| Language: | English |
| Published: |
Cham :
Springer,
2020.
|
| Series: | Lecture notes in computer science ;
12475. LNCS sublibrary. Programming and software engineering. |
| Subjects: |
MARC
| LEADER | 00000cam a2200000xa 4500 | ||
|---|---|---|---|
| 001 | b11500171 | ||
| 003 | CoU | ||
| 005 | 20210212104717.1 | ||
| 006 | m o d | ||
| 007 | cr ||||||||||| | ||
| 008 | 201128s2020 sz o 101 0 eng d | ||
| 019 | |a 1224019724 |a 1225198769 |a 1228050808 |a 1228843651 | ||
| 020 | |a 9783030638825 |q (electronic bk.) | ||
| 020 | |a 3030638820 |q (electronic bk.) | ||
| 020 | |z 9783030638818 | ||
| 020 | |z 3030638812 | ||
| 024 | 7 | |a 10.1007/978-3-030-63882-5 | |
| 035 | |a (OCoLC)spr1224361241 | ||
| 035 | |a (OCoLC)1224361241 |z (OCoLC)1224019724 |z (OCoLC)1225198769 |z (OCoLC)1228050808 |z (OCoLC)1228843651 | ||
| 037 | |a spr978-3-030-63882-5 | ||
| 040 | |a EBLCP |b eng |c EBLCP |d EBLCP |d GW5XE |d OCLCO |d SFB |d LEATE |d YDXIT |d UPM |d YDX |d OCLCF | ||
| 049 | |a GWRE | ||
| 050 | 4 | |a QA76.9.F67 | |
| 111 | 2 | |a Brazilian Symposium on Formal Methods |n (23rd : |d 2020 : |c Online) | |
| 245 | 1 | 0 | |a Formal methods |h [electronic resource] : |b 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings / |c Gustavo Carvalho, Volker Stolz (eds.) |
| 246 | 3 | |a SBMF 2020. | |
| 260 | |a Cham : |b Springer, |c 2020. | ||
| 300 | |a 1 online resource (234 pages) | ||
| 336 | |a text |b txt |2 rdacontent. | ||
| 337 | |a computer |b c |2 rdamedia. | ||
| 338 | |a online resource |b cr |2 rdacarrier. | ||
| 347 | |a text file. | ||
| 347 | |b PDF. | ||
| 490 | 1 | |a Lecture notes in computer science ; |v 12475. | |
| 490 | 1 | |a LNCS sublibrary, SL 2, Programming and software engineering. | |
| 500 | |a International conference proceedings. | ||
| 500 | |a "The conference was supposed to be held in Ouro Preto, Brazil, during November 25-27, 2020. However, in light of the COVID-19 pandemic, it was replaced by a virtual event only on the same dates."-- Preface. | ||
| 505 | 0 | |a Intro -- Preface -- Organization -- Contents -- Invited Talks -- Formal Verification of Neural Networks? -- 1 Introduction -- 2 Verification vs. Validation vs. Trustworthy AI -- 3 Property-Directed Verification of Recurrent Neural Networks -- 4 Conclusion -- References -- Navigating the Universe of Z3 Theory Solvers -- 1 Introduction -- 1.1 Present and Future -- 2 CDCL(T) -- In the Light of Theory Solvers -- 2.1 Invariants -- 3 Boolean Theories -- 4 Base Theories -- 4.1 Arithmetic -- 4.1.1 Rational Linear Arithmetic -- 4.1.2 Integer Linear Arithmetic -- 4.1.3 Non-linear Arithmetic. | |
| 505 | 8 | |a 5 Reducible Theories -- 5.1 Refinement Types -- 5.2 Reducible Theories in Z3 -- 5.2.1 Arrays -- 5.2.2 Floating Points -- 5.2.3 Algebraic Datatypes -- 6 Hybrid Theories -- 7 External Theories -- 8 Conclusion -- References -- Revisiting Refactoring Mechanics from Tool Developers' Perspective -- 1 Introduction -- 2 Motivating Example -- 3 Technique -- 3.1 JDolly -- 3.2 Overview -- 3.3 Detecting Differences in Refactoring Implementations -- 4 Evaluation -- 4.1 Experiment Definition -- 4.2 Results and Discussion -- 4.3 Threats to Validity -- 5 Related Work -- 6 Conclusion -- References. | |
| 505 | 8 | |a Experience Reports -- Safety Assurance of a High Voltage Controller for an Industrial Robotic System -- 1 Introduction -- 2 HVC and Previously Detected Errors -- 2.1 Properties for Formal Verification -- 3 Finite State Machine Modelling -- 4 Model Checking -- 4.1 Model Checking in RoboTool -- 4.2 Model Checking in Simulink Design Verifier (SDV) -- 5 Concluding Remarks and Future Work -- References -- Statistical Model Checking in Drug Repurposing for Alzheimer's Disease -- 1 Introduction -- 2 Background -- 2.1 Statistical Model Checking-SMC -- 2.2 Alzheimer's Disease Pathophysiology. | |
| 505 | 8 | |a 2.3 PI3K/AKT/mTOR Pathway and Alzheimer Disease -- 3 Formal Model -- 3.1 Related Work -- 3.2 The Proposed Model -- 4 Results -- 4.1 Simulations -- 4.2 Effect of Rapamycin in Tau -- 4.3 Effect of Rapamycin in A -- 4.4 Discussion -- 5 Conclusion -- References -- Models, Languages and Semantics -- Calculational Proofs in Relational Graphical Linear Algebra -- 1 Introduction -- 2 Syntax and Semantics of Graphical Linear Algebra -- 2.1 Syntax -- 2.2 Semantics -- 2.3 Diagrammatic Reasoning -- 3 Algebraic Structure -- 3.1 Bialgebra Structure -- 4 Applications -- 4.1 Dictionary. | |
| 505 | 8 | |a 4.2 Classical Existence Theorems -- 4.3 Dotted Line Associativity in Block Linear Algebra -- 5 Conclusions and Future Work -- References -- Modeling Big Data Processing Programs -- 1 Introduction -- 2 Background -- 3 Modeling Big Data Processing Programs -- 3.1 Data Flow -- 3.2 Data Sets and Transformations -- 3.3 Abstracting Features from Big Data Processing Systems -- 4 Applications of the Model -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Optimization of Timed Scenarios -- 1 Introduction -- 2 A General, Flexible Optimisation Algorithm -- 2.1 Preliminaries. | |
| 500 | |a Includes author index. | ||
| 520 | |a This book constitutes the refereed proceedings of the 23rd Brazilian Symposium on Formal Methods, SBMF 2020, which was supposed to take place in Ouro Preto, Brazil, in November 2020. Instead the symposium took place virtually due to the COVID-19 pandemic. The 10 regular papers presented together with 3 invited talks in this book were carefully reviewed and selected from 17 submissions. The papers are organized in topical sections such as: experience reports; models, languages and semantics; and software product lines. Chapter 'Safety Assurance of a High Voltage Controller for an Industrial Robotic System' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. | ||
| 588 | 0 | |a Online resource; title from PDF title page (SpringerLink, viewed February 4, 2021) | |
| 650 | 0 | |a Formal methods (Computer science) |v Congresses. |0 http://id.loc.gov/authorities/subjects/sh2008104061. | |
| 650 | 7 | |a Algorithms. |2 fast |0 (OCoLC)fst00805020. | |
| 650 | 7 | |a Artificial intelligence. |2 fast |0 (OCoLC)fst00817247. | |
| 650 | 7 | |a Computer logic. |2 fast |0 (OCoLC)fst00872265. | |
| 650 | 7 | |a Logic, Symbolic and mathematical. |2 fast |0 (OCoLC)fst01002068. | |
| 650 | 7 | |a Software engineering. |2 fast |0 (OCoLC)fst01124185. | |
| 700 | 1 | |a Carvalho, Gustavo. |0 http://id.loc.gov/authorities/names/no2020055158. | |
| 700 | 1 | |a Stolz, V. |q (Volker) |0 http://id.loc.gov/authorities/names/no2008124383 |1 http://isni.org/isni/0000000053981181. | |
| 776 | 0 | 8 | |i Print version: |a Carvalho, Gustavo |t Formal Methods: Foundations and Applications |d Cham : Springer International Publishing AG,c2021 |z 9783030638818. |
| 830 | 0 | |a Lecture notes in computer science ; |v 12475. |0 http://id.loc.gov/authorities/names/n42015162. | |
| 830 | 0 | |a LNCS sublibrary. |n SL 2, |p Programming and software engineering. |0 http://id.loc.gov/authorities/names/no2007033954. | |
| 856 | 4 | 0 | |u https://colorado.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-030-63882-5 |z Full Text (via Springer) |
| 907 | |a .b115001712 |b 03-02-21 |c 12-15-20 | ||
| 998 | |a web |b 02-28-21 |c b |d b |e - |f eng |g sz |h 0 |i 1 | ||
| 907 | |a .b115001712 |b 03-01-21 |c 12-15-20 | ||
| 944 | |a MARS - RDA ENRICHED | ||
| 915 | |a I | ||
| 956 | |a Springer e-books | ||
| 956 | |b Springer Computer Science eBooks 2020 English+International | ||
| 999 | f | f | |i 5dc446bb-2b45-5de9-ac35-fb1ce491f058 |s d15b5cdd-1ebd-5d78-998b-d27f085f629a |
| 952 | f | f | |p Can circulate |a University of Colorado Boulder |b Online |c Online |d Online |e QA76.9.F67 |h Library of Congress classification |i Ebooks, Prospector |n 1 |