Clockwork finance: Automated analysis of economic security in smart contracts
We introduce the Clockwork Finance Framework (CFF), a general purpose, formal
verification framework for mechanized reasoning about the economic security properties of …
verification framework for mechanized reasoning about the economic security properties of …
A survey of challenges for runtime verification from advanced application domains (beyond software)
Runtime verification is an area of formal methods that studies the dynamic analysis of
execution traces against formal specifications. Typically, the two main activities in runtime …
execution traces against formal specifications. Typically, the two main activities in runtime …
The imandra automated reasoning system (system description)
G Passmore, S Cruanes, D Ignatovich, D Aitken… - … : 10th International Joint …, 2020 - Springer
We describe Imandra, a modern computational logic theorem prover designed to bridge the
gap between decision procedures such as SMT, semi-automatic inductive provers of the …
gap between decision procedures such as SMT, semi-automatic inductive provers of the …
Milestones from the Pure Lisp theorem prover to ACL2
JS Moore - Formal Aspects of Computing, 2019 - Springer
We discuss the evolutionary path from the Edinburgh Pure Lisp Theorem Prover of the early
1970s to its modern counterpart, AC omputational L ogic for A pplicative C ommon L isp, aka …
1970s to its modern counterpart, AC omputational L ogic for A pplicative C ommon L isp, aka …
A modern compiler for the french tax code
In France, income tax is computed from taxpayers' individual returns, using an algorithm that
is authored, designed and maintained by the French Public Finances Directorate (DGFiP) …
is authored, designed and maintained by the French Public Finances Directorate (DGFiP) …
Some lessons learned in the industrialization of formal methods for financial algorithms
GO Passmore - Formal Methods: 24th International Symposium, FM …, 2021 - Springer
At Imandra Inc. we have pioneered the application of formal methods to financial algorithms
[3]. After nearly a decade of R&D and business development, our Imandra automated …
[3]. After nearly a decade of R&D and business development, our Imandra automated …
Summing up smart transitions
Some of the most significant high-level properties of currencies are the sums of certain
account balances. Properties of such sums can ensure the integrity of currencies and …
account balances. Properties of such sums can ensure the integrity of currencies and …
An integrated development environment for the prototype verification system
The steep learning curve of formal technologies is a well-known barrier to the adoption of
formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated …
formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated …
Sabrina: Modeling and visualization of financial data over time with incremental domain knowledge
Investment planning requires knowledge of the financial landscape on a large scale, both in
terms of geo-spatial and industry sector distribution. There is plenty of data available, but it is …
terms of geo-spatial and industry sector distribution. There is plenty of data available, but it is …
ACL2s systems programming
AT Walter, P Manolios - arXiv preprint arXiv:2205.11704, 2022 - arxiv.org
ACL2 provides a systems programming capability that allows one to write code that uses
and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the …
and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the …