Hoare Logic for Realistically Modelled Machine Code

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

Download Full-text

Polymorphic type inference for machine code

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2016 ◽

10.1145/2908080.2908119 ◽

2016 ◽

Cited By ~ 8

Author(s):

Matt Noonan ◽

Alexey Loginov ◽

David Cok

Keyword(s):

Type Inference ◽

Machine Code ◽

Polymorphic Type

Download Full-text

Compiler Module of Abstract Machine Code for Formal Semantics Course

2021 IEEE 19th World Symposium on Applied Machine Intelligence and Informatics (SAMI) ◽

10.1109/sami50585.2021.9378696 ◽

2021 ◽

Author(s):

William Steingartner

Keyword(s):

Formal Semantics ◽

Machine Code ◽

Abstract Machine

Download Full-text

CSim 2

ACM Transactions on Programming Languages and Systems ◽

10.1145/3436808 ◽

2021 ◽

Vol 43 (1) ◽

pp. 1-46

Author(s):

David Sanan ◽

Yongwang Zhao ◽

Shang-Wei Lin ◽

Liu Yang

Keyword(s):

Programming Languages ◽

Concurrent Systems ◽

Theorem Prover ◽

Compositional Techniques ◽

Machine Code ◽

Top Down ◽

Hol Theorem Prover ◽

High Level ◽

High Degree

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

Download Full-text