Browse All Reviews
Software Engineering (D.2)
Software/Program Verification (D.2.4)
> Formal Methods (D.2.4...)
All Media Types
1-10 of 123 Reviews about "
Formal Methods (D.2.4...)
Parallel cost analysis
Albert E., Correas J., Johnsen E., Pun K., Román-Díez G. ACM Transactions on Computational Logic 19(4): 1-37, 2018. Type: Article
In this paper, the authors present “static cost analysis for distributed systems that exploits the parallelism among distributed locations to infer a more precise estimation of the parallel cost.” Such a parallel cost analysis can be o...
Apr 2 2021
Systematically ensuring the confidence of real-time home automation IoT systems
Bu L., Xiong W., Liang C., Han S., Zhang D., Lin S., Li X. ACM Transactions on Cyber-Physical Systems 2(3): 1-23, 2018. Type: Article
The quick expansion of computing technology in many areas leads to different new paradigms; among them is the paradigm of cyber-physical systems (CPS) with commonly acquired sensor data that can be processed in real time. One of the manifestations...
Oct 13 2020
Formal methods: an appetizer
Nielson F., Nielson H., Springer International Publishing, New York, NY, 2019. 162 pp. Type: Book (978-3-030051-55-6)
I’ve occasionally been intimidated into ordering an appetizer as the main course, but have rarely regretted it thanks to the presence of “gourmet” friends. This is an excellent, ultra-elegant, and rigorous book. Its 160 printed p...
Apr 23 2020
Modular product programs
Eilers M., Müller P., Hitz S. ACM Transactions on Programming Languages and Systems 42(1): 1-37, 2019. Type: Article
Some properties of programs are not about a single run of the program; instead, they relate multiple runs. For example, a program is deterministic if, given the same input, two runs will always produce the same answer. Many other properties of int...
Jan 14 2020
Verification methods for the computationally complete symbolic attacker based on indistinguishability
Bana G., Chadha R., Eeralla A., Okada M. ACM Transactions on Computational Logic 21(1): 1-44, 2019. Type: Article
First-order logic formalization for security protocols and attackers enables formal verification. Once a formalization is established, standard tools such as a theorem prover can be used in the analysis....
Dec 16 2019
Reproducibility in scientific computing
Ivie P., Thain D. ACM Computing Surveys 51(3): 1-36, 2018. Type: Article
The authors discuss reproducible research, that is, research where the same task produces the same result as the original research. Researchers in the computing community are encouraged to make their results reproducible so that others can verify,...
Nov 19 2019
Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems
Cauchi N., Laurenti L., Lahijanian M., Abate A., Kwiatkowska M., Cardelli L. HSCC 2019 (Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, Apr 16-18, 2019) 240-251, 2019. Type: Proceedings
Hybrid systems are those “with both continuous dynamics and discrete logic” . The discrete logic serves to label or parametrize (my terms) states; state-specific continuous dynamics, modeled largely if not exclusively by differentia...
Jul 12 2019
Inferring extended probabilistic finite-state automaton models from software executions
Emam S., Miller J. ACM Transactions on Software Engineering and Methodology 27(1): 1-39, 2018. Type: Article
To facilitate the testing and maintenance of software systems, researchers have generated behavioral models in the form of finite-state automata from software execution traces. Even though a finite-state automaton (FSA) is a common dynamic model i...
Oct 25 2018
CoSMed: a confidentiality-verified social media platform
T., Pesenti Gritti A., Popescu A., Raimondi F. Journal of Automated Reasoning 61(1-4): 113-139, 2018. Type: Article
What do we mean when we say that a system is verified? In theory it means that certain properties of a system have been proved to hold. In practice, the answer is rather more complicated....
Aug 22 2018
Computer arithmetic and formal proofs: verifying floating-point algorithms with the Coq system
Boldo S., Melquiond G., ISTE Press - Elsevier, London, UK, 2017. 326 pp. Type: Book (978-1-785481-12-3)
The audience for this superlatively researched and crafted book includes postgraduate students and practitioners of floating-point (FP) computation or formal verification. The authors “sincerely hope that, after reading this book, you will f...
Aug 8 2018
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.