Related papers: Contract Strengthening through Constrained Horn Cl…
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of…
While smart contracts are foundational elements of blockchain applications, their inherent susceptibility to security vulnerabilities poses a significant challenge. Existing training datasets employed for vulnerability detection tools may…
Dual Horn clauses mirror key properties of Horn clauses. This paper explores the ``other side of the looking glass'' to reveal some expected and unexpected symmetries and their practical uses. We revisit Dual Horn clauses as enablers of a…
Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a…
Contract consistency is important in ensuring the legal validity of the contract. In many scenarios, a contract is written by filling the blanks in a precompiled form. Due to carelessness, two blanks that should be filled with the same (or…
Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum…
We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and…
Nowadays, smart contracts have become increasingly popular and, as with software development in general, testing is the standard method for verifying their correctness. However, smart contracts require a higher level of certainty regarding…
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have…
As a blockchain platform that has developed vigorously in recent years, Ethereum is different from Bitcoin in that it introduces smart contracts into blockchain.Solidity is one of the most mature and widely used smart contract programming…
Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art…
Horn-satisfiability or Horn-SAT is the problem of deciding whether a satisfying assignment exists for a Horn formula, a conjunction of clauses each with at most one positive literal (also known as Horn clauses). It is a well-known…
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this…
Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there…
Our scientific knowledge is increasingly built on software output. User code which defines data analysis pipelines and computational models is essential for research in the natural and social sciences, but little is known about how to…
We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification…
The correctness of a structured program is, at best, plausible. Though this is a step forward compared to what came before, it falls short of verified correctness. To verify a structured program according to Hoare's method one is faced with…
Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to decompose a large contextual refinement into many smaller…
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this…
This paper contributes to the verification of programs written in Bitcoin's smart contract language SCRIPT in the interactive theorem prover Agda. It focuses on the security property of access control for SCRIPT programs that govern the…