Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications

10.36227/techrxiv.14096576 ◽

2021 ◽

Author(s):

Jayaraj Poroor

Keyword(s):

Natural Language ◽

Formal Verification ◽

Domain Knowledge ◽

Semantic Content ◽

Hoare Logic ◽

Critical Systems ◽

Semantic Parsing ◽

Natural Language Text ◽

Safety Requirements ◽

Formal Framework

Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against specifications in the form of pre-condition/post-condition assertions. The advancement of semantic parsing techniques and higher computational capabilities enable us to extract semantic content from natural language text as formal logical forms, with increasing accuracy and coverage. This paper proposes a formal framework for Hoare logic-based formal verification of imperative programs using logical forms generated from compositional semantic parsing of natural language assertions. We call our reasoning approach Natural Hoare Logic. This enables formal verification of software directly against safety requirements specified by a domain expert in natural language. We consider both declarative assertions of program invariants and state change as well as imperative assertions that specify commands which alter the program state. We discuss how the reasoning approach can be extended using domain knowledge and a practical approach for guarding against semantic parser errors.

Download Full-text

Automatic Source Code Summarization using Semantics and Stereotypes

International Journal of Recent Technology and Engineering - 2 ◽

10.35940/ijrte.d7774.118419 ◽

2019 ◽

Vol 8 (4) ◽

pp. 599-604

Keyword(s):

Natural Language ◽

Traditional Approach ◽

Source Code ◽

Final Analysis ◽

Semantic Content ◽

Complex Tasks ◽

Natural Language Text ◽

Language Text

In Software industries developers and testers spend most of the time in code maintainability than in developing or testing the code. Even after spending lot of time in analyzing the code the final analysis will serve only 50% of their purpose. The analysis involves many complex tasks like code comprehension, code extensibility and code portability. The traditional approach is to analyze the code manually, which is a tedious and time consuming task. Existing techniques does not provide the required summary, most of them are complex and they are not in natural language format. In this paper we propose a novel summarization technique that summarizes the source code similar to natural language text. The proposed system provides summary is based on the semantic content in the source code, in case the source code does not contain semantic contents it uses the java stereotypes to get the semantic content. The proposed system delivers the summaries which simplifies the task of the developer and provides the required summary.

Download Full-text

Formal Verification of Control System Software

10.23943/princeton/9780691181301.001.0001 ◽

2019 ◽

Author(s):

Pierre-Loïc Garoche

Keyword(s):

Control System ◽

Formal Verification ◽

Formal Analysis ◽

Critical Systems ◽

System Software ◽

Unified Approach ◽

Verification Methods ◽

Autonomous Cars ◽

Computer Scientists ◽

Verification Techniques

The verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. This book provides control engineers and computer scientists with an introduction to the formal techniques for analyzing and verifying this important class of software. Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. The book provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. It presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software. As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

Download Full-text

Morality Classification in Natural Language Text

IEEE Transactions on Affective Computing ◽

10.1109/taffc.2020.3034050 ◽

2020 ◽

pp. 1-1

Author(s):

Matheus C. Pavan ◽

Vitor G. Santos ◽

Alex G. J. Lan ◽

Joao Martins ◽

Wesley Ramos Santos ◽

...

Keyword(s):

Natural Language ◽

Natural Language Text ◽

Language Text

Download Full-text

Natural language processing methods for knowledge management—Applying document clustering for fast search and grouping of engineering documents

Concurrent Engineering ◽

10.1177/1063293x20982973 ◽

2021 ◽

pp. 1063293X2098297

Author(s):

Ivar Örn Arnarsson ◽

Otto Frost ◽

Emil Gustavsson ◽

Mats Jirstrand ◽

Johan Malmqvist

Keyword(s):

Natural Language Processing ◽

Natural Language ◽

Language Processing ◽

Domain Knowledge ◽

Clustering Algorithms ◽

Document Clustering ◽

Unstructured Data ◽

Free Text ◽

Engineering Change ◽

Engineering Documents

Product development companies collect data in form of Engineering Change Requests for logged design issues, tests, and product iterations. These documents are rich in unstructured data (e.g. free text). Previous research affirms that product developers find that current IT systems lack capabilities to accurately retrieve relevant documents with unstructured data. In this research, we demonstrate a method using Natural Language Processing and document clustering algorithms to find structurally or contextually related documents from databases containing Engineering Change Request documents. The aim is to radically decrease the time needed to effectively search for related engineering documents, organize search results, and create labeled clusters from these documents by utilizing Natural Language Processing algorithms. A domain knowledge expert at the case company evaluated the results and confirmed that the algorithms we applied managed to find relevant document clusters given the queries tested.

Download Full-text

Formal verification of algorithms for critical systems

ACM SIGSOFT Software Engineering Notes ◽

10.1145/123041.123044 ◽

1991 ◽

Vol 16 (5) ◽

pp. 1-15 ◽

Cited By ~ 4

Author(s):

John Rushby ◽

Friedrich von Henke

Keyword(s):

Formal Verification ◽

Critical Systems

Download Full-text

Large-scale Semantic Parsing without Question-Answer Pairs

Transactions of the Association for Computational Linguistics ◽

10.1162/tacl_a_00190 ◽

2014 ◽

Vol 2 ◽

pp. 377-392 ◽

Cited By ~ 40

Author(s):

Siva Reddy ◽

Mirella Lapata ◽

Mark Steedman

Keyword(s):

Natural Language ◽

Large Scale ◽

Graph Matching ◽

State Of The Art ◽

The State ◽

Semantic Parsing ◽

Matching Problem ◽

Weak Supervision ◽

Benchmark Datasets

In this paper we introduce a novel semantic parsing approach to query Freebase in natural language without requiring manual annotations or question-answer pairs. Our key insight is to represent natural language via semantic graphs whose topology shares many commonalities with Freebase. Given this representation, we conceptualize semantic parsing as a graph matching problem. Our model converts sentences to semantic graphs using CCG and subsequently grounds them to Freebase guided by denotations as a form of weak supervision. Evaluation experiments on a subset of the Free917 and WebQuestions benchmark datasets show our semantic parser improves over the state of the art.

Download Full-text