HackerPapers

arXiv:1809.03162cs.LO

A case study in formal verification of a Java program

Dmitry Brizhinev, Rajeev Goré

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and select Krakatoa as the most appropriate for the task. Based on our experience, we present several suggestions for making the tools more user friendly, which we hope will lead to wider adoption of formal methods. In particular, we discuss at length how useful it would be for provers to perform some form of abduction, that is, for them to guess which extra assumptions they need to prove a statement. It is our opinion that progress in this area would produce the largest improvement in the usability of formal verification tools.

arXiv comments
Written in August 2016
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Jul 2020 to Jul 2020.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Ask HN: Why don't you use formal methods? 1 comment

    • Maybe this is just my ignorance speaking, but I think that using formal methods would take a lot of time; more than the projects I am working on are worth. Also, I don't know how to do it. I mean, at school we had some examples, but those were for math-like stuff (how to verify…

      Viliam1234View on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.