Related papers: Source Code Verification for Embedded Systems usin…
We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we…
In this paper we present ProSLAM, a lightweight stereo visual SLAM system designed with simplicity in mind. Our work stems from the experience gathered by the authors while teaching SLAM to students and aims at providing a highly modular…
This short paper describes a simple and intuitive Prolog program, a metainterpreter, that computes the bottom up meaning of a simple positive Horn clause definition. It involves a simple transformation of the object program rules into…
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge…
Static analysis approximates the results of a program by examining only its syntax. For example, control-flow analysis (CFA) determines which syntactic lambdas (for functional languages) or (for object-oriented) methods may be invoked at…
Formal verification is increasingly recognized as a critical foundation for building reliable software systems. However, the need for specialized expertise to write precise specifications, navigate complex proof obligations, and learn…
Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and…
In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the significant sources of security vulnerabilities. However, there exist only a few attempts with limited success to cope…
The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $\mu$SPEC models. Despite the efficacy of this approach, a verification gap between…
Smart contracts have been increasingly used together with blockchains to automate financial and business transactions. However, many bugs and vulnerabilities have been identified in many contracts which raises serious concerns about smart…
Deep learning techniques applied to program analysis tasks such as code classification, summarization, and bug detection have seen widespread interest. Traditional approaches, however, treat programming source code as natural language text,…
Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery (CI/CD). However, this decentralized development by separate teams and…
Large language models (LLMs) are increasingly used to generate requirements specifications, design documents, code, and test cases. In contrast, much less attention has been given to a more difficult assurance problem: statically verifying…
In this paper two intensive problems faced during software application's analysis and development process arose by the software industry are briefly conversed i.e. identification of fault proneness and increase in rate of variability in the…
How to apply automated verification technology such as model checking and static program analysis to millions of lines of embedded C/C++ code? How to package this technology in a way that it can be used by software developers and engineers,…
Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these…
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a…
This thesis concerns the implementation of Lambda Prolog, a higher-order logic programming language that supports the lambda-tree syntax approach to representing and manipulating formal syntactic objects. Lambda Prolog achieves its…
Currently, while software engineers write code for various modules, quite often, various types of errors - coding, logic, semantic, and others (most of which are not caught by compilation and other tools) get introduced. Some of these bugs…
Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying programs operating upon Boolean and integer values (e.g.…