PoTR: Accurate and Efficient Proof of Timely-Retrievability for Storage Systems
The use of remote storage has become prevalent both by organizations and individuals. By relying on third-party storage, such as cloud or peer-to-peer storage services, availability, fault tolerance, and low access latency can be attained in a cost-...
Automated Generation of Modular Assurance Cases with the System Assurance Reference Model
Assurance cases are structured arguments used to demonstrate specific system properties such as safety or security. They are used in many industrial sectors including automotive, aviation and medical devices. Assurance cases are usually divided into ...
ω-Regular Energy Problems
We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. ...
Empirical architecture comparison of two-input machine learning systems for vision tasks
As machine learning models have been deployed in many vision systems including autonomous vehicles and robots, designing architectures for machine learning systems (MLSs) has emerged as a critical concern. Previous studies have shown that enhancing the ...
A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems
A calculus for the specification and verification of distributed concurrent interactive real time systems is introduced. Systems are specified by their interface behavior formalized by interface predicates and interface assertions. System designs in terms ...
Does Every Computer Scientist Need to Know Formal Methods?
- Manfred Broy,
- Achim Brucker,
- Alessandro Fantechi,
- Mario Gleirscher,
- Klaus Havelund,
- Markus Alexander Kuppe,
- Alexandra Mendes,
- André Platzer,
- Jan Ringert,
- Allison Sullivan
We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs ...
SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics
Parameter identifiability is an important aspect of parameter estimation of dynamic system modelling. Several methods exist to determine identifiability of parameter sets using the model definition and analysis of experimental data. There is also the ...
Trace Semantics for C++11 Memory Model
The C and C++ languages introduced the relaxed-memory concurrency into the language specification for efficiency purposes in 2011.
Trace semantics can provide the mathematical foundation for the proposed C++11 memory model, and there is a lack of ...
SecCT: Secure and scalable count query models on encrypted genomic data
Recently, due to the continued reduction in DNA sequencing cost, large-scale genetic samples are being gathered for accelerating predispositions to specific diseases, tailoring treatment of efficient drugs and therapies, etc. Massive genetic samples are ...
On Formal Methods Thinking in Computer Science Education
- Brijesh Dongol,
- Catherine Dubois,
- Stefan Hallerstede,
- Eric Hehner,
- Carroll Morgan,
- Peter Müller,
- Leila Ribeiro,
- Alexandra Silva,
- Graeme Smith,
- Erik de Vink
Formal Methods (FM) radically improve the quality of the code artefacts they help to produce. They are simple, probably accessible to first-year undergraduate students and certainly to second-year students and beyond. Nevertheless, in many cases, they are ...
Using Multi-dimensional Quorums for Optimal Resilience in Multi-resource Blockchains
Permissionless blockchains commonly use resource challenges to defend against sybil attacks. For example, popular resource challenge designs include Proof-of-Work and Proof-of-Stake. It is well-known that simultaneously exploiting multiple resources can ...
RNA: R1CS Normalization Algorithm Based on Data Flow Graphs for Zero-Knowledge Proofs
The communities of blockchains and distributed ledgers have been stirred up by the introduction of zero-knowledge proofs (ZKPs). Originally designed as a solution to privacy issues, ZKPs have now evolved into an effective remedy for scalability concerns. ...
A compositional simulation framework for Abstract State Machine models of Discrete Event Systems
Modeling complex system requirements often requires specifying system components in separate models, which can be validated and verified in isolation from each other, and then integrating all components’ behavior in order to validate the operation of the ...
