Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings

Invited Presentations

© Springer Nature Switzerland AG 2019

M. H. ter Beek et al. (eds.)Formal Methods – The Next 30 YearsLecture Notes in Computer Science11800https://doi.org/10.1007/978-3-030-30942-8_1

The Human in Formal Methods

Shriram Krishnamurthi¹   and Tim Nelson¹  

(1)

Brown University, Providence, RI, USA

Shriram Krishnamurthi (Corresponding author)

Email: sk@cs.brown.edu

Tim Nelson

Email: tn@cs.brown.edu

Abstract

Formal methods are invaluable for reasoning about complex systems. As these techniques and tools have improved in expressiveness and scale, their adoption has grown rapidly. Sustaining this growth, however, requires attention to not only the technical but also the human side. In this paper (and accompanying talk), we discuss some of the challenges and opportunities for human factors in formal methods.

Keywords

Human factorsUser InterfacesEducationFormal methods

1 Humans and Formal Methods

Formal methods are experiencing a long-overdue surge in popularity. This ranges from an explosion in powerful traditional tools, like proof assistants and model checkers, to embeddings of formal methods in program analysis, to a growing recognition of the value to writing formal properties in other settings (like software testing). Whereas traditionally, corporate use was primarily in hardware (e.g., Seger [26]), now major software companies like Amazon [1, 7, 21], Facebook [6], and Microsoft [3, 12] are growing their use of formal methods.

What does it take to support this growth? Researchers will, naturally, continue to work on formal techniques. We believe, however, that not enough attention has been paid to the humans in the loop. In this paper and accompanying talk, we discuss some of the challenges and opportunities in this area.

To set a context for what follows, our own work has focused largely on automated methods, specifically model finding [18, 34], as typified by tools like Alloy [15] and SAT/SMT solvers. This is not to decry the value of other techniques, including deductive methods, which we have worked with in some of our research. However, we find that model-finding tools offer a useful sweet spot:

Because of their automation, they provide a helpful separation between specification and proof, enabling the user to focus on the former without having to dwell very much on the latter. This separation of concerns is invaluable in training contexts, since it enables us to focus on one skill at a time.

Because model-finders can be used without properties, they enable exploration in addition to verification and proof. Furthermore, this can start with small amounts of partial specification. This idea, which is one aspect of lightweight formal methods [16], is a powerful enabler for quickly seeing the value that formal methods can provide.

The manifestation of these methods in tools like Alloy proves particularly convenient. An Alloy user can write a small part of a specification and click Run (an action already familiar from programming environments), and immediately get at least somewhat useful feedback from the system.

Due to these factors, in our experience, we have found these methods more accessible than others to a broad range of students. Since, in particular, our emphasis is not just on cultivating the small group of hard core students but to bring the other 90% into the fold, tools that immediately appeal to them—and hold their attention, while they are choosing between courses in formal methods and in other exciting areas such as machine learning—are important.

In the rest of this paper, we focus on two human-facing concerns: the human-factors qualities of model finding tools (Sect. 2), and education (Sect. 3). We believe both are vital: the latter to growing the number of people comfortable with formal methods, and the former to their effectiveness.

2 User Experience

We believe that the user experience of formal-methods tools has largely been understudied, although there have been promising past venues such as the Workshops on User Interfaces for Theorem Provers (e.g., [2]) and Human-Oriented Formal Methods (e.g., [19]). The majority of this work focuses on interactive tools such as proof assistants, which is to be expected. For instance, in deductive methods, the experience of stating and executing deduction steps is critical. (For early student-facing work, see the efforts of Barker-Plummer, Barwise, and Etchemendy [4]).

However, other formal tools could also benefit from user-focused research. For instance, model finders are often integrated into higher-level tools (with their model output presented in a domain-specific way). Thus, questions of quality and comprehensibility by lay users are key.

Our own work [8] has found that a model finder’s choice of output and its presentation can make a major difference in user experience. Experiments with students found that output minimality, while intutively appealing, is not necessarily helpful for comprehending systems. Moreover, experiments with users on Amazon’s Mechanical Turk crowdsourcing platform seem to suggest that providing a small amount of additional information alongside output can be helpful for comprehension.

3 Education

An equally important—and critically human-centric—problem is thinking about education. Numerous authors have books that present different educational viewpoints but, to our knowledge, most of these have not been subjected to any rigorous evaluation of effectiveness. Nevertheless, beyond books and curricula, we believe much more attention should be paid to design methods and student-centric tools. There is a large body of literature on these topics in programming education, but its counterparts are often missing in formal methods education.

We are focusing primarily on the task of writing specifications, because:

It is a near-universal requirement shared between different formal methods—indeed, it is perhaps a defining characteristic of the field.

Specifications are sufficiently different from programs that we cannot blindly reuse existing knowledge about programming education, though of course there are many problems in common and we should try to port ideas. If anything, we conjecture that the need for formal methods to consider all possible behaviors, thanks to attributes like non-determinism, might make it harder than programming.

Specifications are useful even outside traditional formal methods settings, such as in property-based testing, monitoring, etc. Hence, they increasingly affect a growing number of programmers, even ones who don’t think of themselves as using traditional formal methods.

We will in turn discuss design methods (Sect. 3.1) and tools (Sect. 3.2).

3.1 A Design Recipe for Writing Specifications

One of the challenges every author faces is the blank page syndrome [9]: given a problem statement, they must fill a blank page (or editor) with magical incantations that match the given statement. For many students, this can be a daunting and even overwhelming experience; ones for whom it is not are sometimes merely overconfident in their abilities.

However, in other design disciplines—from electrical engineering to building architecture—designers produce not just one final artifact but a series of intermediate artifacts, using a range of representations with distinct viewpoints that hide some aspects and make others salient. What might that look like in our discipline?

One answer is provided by How to Design Programs [9], which breaks down the programming process into a series of steps called the Design Recipe. These steps incrementally build towards a solution, alternating abstract and concrete steps that build on previous ones. For programming, these steps are:

1.

Data definitions: translating what is given in the problem statement into abstract descriptions for the computer system.

2.

Data examples: constructing examples of each data definition to ensure the student understands it, has created a well-formed definition, and can cover the cases the problem demands.

3.

Function outline: translating the function expected in the problem into an abstract computational representation, including type signatures, purpose statements, and a function header.

4.

Function examples: constructing input-output examples of the function’s use, using the data examples and the function outline components. These ensure the student actually understands the problem before they start working on it. These are usually written using the syntax of test cases, so they can eventually be run against the final function, but they are conceptually different: they represent exploration and understanding of the problem.

5.

Function template: Using the data definition and function outline to create a skeleton of the body based purely on the structure of the data.

6.

Function definition: Filling in the template to match the specific function definition, using the examples as a guide.

7.

Testing: Constructing tests based on the chosen implementation strategy, checking for implementation-specific invariants. The goal of tests, in contrast to function examples, is to falsify the purported implementation.

There is significant cognitive theory backing the use of this recipe. The process corresponds to Bruner’s notion of scaffolding [31], while the steps reflect Vygotsky’s theory of zones of proximal development [29]. The progression from data through examples to code and tests provides a form of concreteness fading [13]. Completed sequences form worked examples [28] that students can apply to new problems. The templates are a form of program schema [22, 27] that students can recall and reuse in constructing solutions to new problems.

How can we translate this from writing programs to writing specifications? We believe many of the steps carry over directly (and serve the same purpose), while others need some adaptation, depending on what students are authoring (the process for specifications would look different than that for models given to a model-checker, etc.). For instance, the function examples stage translates well to students creating concrete instances of behavior that they believe should or should not satisfy the eventual specification.

We will not go here into the details of how to adapt this process to different settings, especially authoring specifications. However, we believe the basic ideas are fairly universal: of proceeding in a step-wise way with new artifacts building on old artifacts; of proceeding from the concrete to the abstract; of writing illustrative, concrete examples of preceding abstract steps to test well-formedness and understanding; and so on.

3.2 Tools

Researchers and developers have invested significant effort into formal methods tools, many of which are then brought into the classroom. On the one hand, industrial-strength tools tend to be robust and performant, and are endowed with authenticity, which can make a difference for some students. On the other hand, they may expose too much power: they accept full and complex languages that contain features that may confuse students, they produce errors and other feedback with terminology that students may not understand, and so on. In light of this, projects have advocated the use of language levels [5, 10, 14], arguing that students would benefit from a graduated introduction through a sequence of sub-languages (and corresponding tool interfaces), each sub-language presenting an epistemic closure that corresponds to a student’s learning at that point.

Beyond this, we argue that educational settings have one key advantage that conventional industrial use does not: the presence of ground truth, i.e., someone already knows the answer! In industry, users rarely build a whole new specification that precisely matches one that already exists. In education, however, that is exactly what students do almost all the time. Therefore, we can ask:

How does the presence of a ground truth affect formal tools in education?

We argue that knowing the answer especially helps in light of the Design Recipe discussed above, because we can build tools to help with each step. We discuss a concrete manifestation of this below. These should be thought of as training wheels to help beginners become comfortable with formal methods; naturally, we need to study how to wean students so that they can engage in the more authentic experience of writing specifications and models un-aided.

Understanding Before Authoring. A growing body of literature in programming education [17, 25, 30] shows that students frequently start to write programs before they have understood the problem. As a result they solve the wrong problem entirely. Not only is this frustrating, it also leads to learning loss: the stated problem presumably had certain learning goals, which the student may not have met as a result of their misdirection.

Recent work [24, 32] has begun to address this issue by devising techniques to make sure students can check their understanding of the problem before they embark on a solution. These critically rely on having intermediate artifacts authored by the student in the process of authoring, precisely matching the intermediate steps proposed by the Design Recipe. In particular, function examples are a valuable way for them to demonstrate their understanding; because they are written in executable form, they can be run against implementations.

We especially draw on the perspective of Politz et al. [23] and Wrenn et al. [33], which think of tests (and examples) as classifiers. That is, the quality of a suite of tests or examples can be judged by how well they classify a purported implementation as correct or faulty. If we want a quantitative result, we can compute precision and recall scores to characterize these classifiers. Thus, students can rapidly obtain concrete feedback about how well they are doing in terms of understanding the problem, and our evidence in the context of programming [32] suggests that they take great advantage of this. Initial explorations for specification authoring suggests that this phenomenon carries over.

More Artifacts. More broadly, there are several artifacts that can be produced on both sides for specification-authoring assignments, including:

Student’s concrete examples

Student’s properties

Student’s completed specification

Instructor’s concrete examples

Instructor’s properties

Instructor’s completed specification

the latter three of which are ground truth components. Furthermore, instructional staff can be pressed to produce multiple kinds of each of these, such as correct and faulty specifications to enable classification.

Given this rich set of artifacts, it is instructive to consider all their (at least) pairwise combinations. For example, consider the point where the student believes they have completed their specification. This can now be compared for semantic difference [11, 20] against the instructor’s specification, with the differences presented as concrete examples that the student has to determine how to incorporate to adjust their specification. There are several interesting questions of mechanism design, i.e., how to structure rewards and penalties for students using these modes.

4 Conclusion

In sum, we believe there are large human-facing aspects of formal methods that have not yet been explored, and that exploring them is vital for the field to thrive. With enough emphasis, we believe formal methods can be democratized and made accessible to large numbers of users—not only scientists and trained operators, but even the general public, from children to retirees. Even the most non-technical user has to make consequential decisions every time they set a configuration option on a system, and would hence benefit from the specification and state-exploration powers that characterize our field. These problems are intellectually exciting and challenging, and serious progress requires wedding technical results to cognitive and social ones.

Acknowledgements

This work was partially supported by the U.S. National Science Foundation. We are grateful for numerous valuable conversations with Daniel J. Dougherty, Natasha Danas, Jack Wrenn, Kathi Fisler, Daniel Jackson, and Emina Torlak.

References

1.

Amazon Web Services: Provable security. https://​aws.​amazon.​com/​security/​provable-security/​. Accessed 5 July 2019

2.

Autexier, S., Benzmüller, C. (eds.): User Interfaces for Theorem Provers, Proceedings of UITP 2006, Electronic Notes in Theoretical Computer Science, vol. 174. Elsevier (2007)

3.

Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004). https://​doi.​org/​10.​1007/​978-3-540-24756-2_​1Crossref

4.

Barker-Plummer, D., Barwise, J., Etchemendy, J.: Language, Proof, and Logic, 2nd edn. Center for the Study of Language and Information/SRI, Stanford (2011)zbMATH

5.

du Boulay, B., O’Shea, T., Monk, J.: The black box inside the glass box. Int. J. Hum.-Comput. Stud. 51(2), 265–277 (1999)Crossref

6.

Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://​doi.​org/​10.​1007/​978-3-319-17524-9_​1Crossref

7.

Cook, B.: Formal reasoning about the security of amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 38–47. Springer, Cham (2018). https://​doi.​org/​10.​1007/​978-3-319-96145-3_​3Crossref

8.

Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168–184. Springer, Cham (2017). https://​doi.​org/​10.​1007/​978-3-319-66197-1_​11Crossref

9.

Felleisen, M., Findler, R.B., Flatt, M., Krishnamurthi, S.: How to Design Programs, 2nd edn. MIT Press, Cambridge (2018). https://​www.​htdp.​org/​zbMATH

10.

Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Prog. 12(2), 159–182 (2002)MathSciNetCrossref

11.

Fisler, K., Krishnamurthi, S., Meyerovich, L., Tschantz, M.: Verification and change impact analysis of access-control policies. In: International Conference on Software Engineering, pp. 196–205 (2005)

12.

Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation (2015)

13.

Fyfe, E.R., McNeil, N.M., Son, J.Y., Goldstone, R.L.: Concreteness fading in mathematics and science instruction: a systematic review. Educ. Psychol. Rev. 26(1), 9–25 (2014)Crossref

14.

Holt, R.C., Wortman, D.B.: A sequence of structured subsets of PL/I. SIGCSE Bull. 6(1), 129–132 (1974)Crossref

15.

Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2012)

16.

Jackson, D., Wing, J.: Lightweight formal methods. IEEE Comput. (1996)

17.

Loksa, D., Ko, A.J.: The role of self-regulation in programming problem solving process and success. In: SIGCSE International Computing Education Research Conference (2016)

18.

McCune, W.: Mace4 reference manual and guide. CoRR (2003). https://​arxiv.​org/​abs/​cs.​SC/​0310055

19.

Milazzo, P., Varró, D., Wimmer, M. (eds.): STAF 2016. LNCS, vol. 9946. Springer, Cham (2016). https://​doi.​org/​10.​1007/​978-3-319-50230-4Crossref

20.

Nelson, T., Ferguson, A.D., Krishnamurthi, S.: Static differential program analysis for software-defined networks. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 395–413. Springer, Cham (2015). https://​doi.​org/​10.​1007/​978-3-319-19249-9_​25Crossref

21.

Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)Crossref

22.

Pirolli, P.L., Anderson, J.R.: The role of learning from examples in the acquisition of recursive programming skills. Canadian Journal of Psychology/Revue canadienne de psychologie 39(2), 240–272 (1985)Crossref

23.

Politz, J.G., Krishnamurthi, S., Fisler, K.: In-flow peer-review of tests in test-first programming. In: Conference on International Computing Education Research (2014)

24.

Prather, J., et al.: First things first: providing metacognitive scaffolding for interpreting problem prompts. In: ACM Technical Symposium on Computer Science Education (2019)

25.

Prather, J., Pettit, R., McMurry, K., Peters, A., Homer, J., Cohen, M.: Metacognitive difficulties faced by novice programmers in automated assessment tools. In: SIGCSE International Computing Education Research Conference (2018)

26.

Seger, C.H.: Combining functional programming and hardware verification (abstract of invited talk). In: International Conference on Functional Programming (ICFP) (2000)

27.

Spohrer, J.C., Soloway, E.: Simulating Student Programmers. In: IJCAI 1989, pp. 543–549. Morgan Kaufmann Publishers Inc. (1989)

28.

Sweller, J.: The worked example effect and human cognition. Learn. Instr. 16(2), 165–169 (2006)Crossref

29.

Vygotsky, L.S.: Mind in Society: The Development of Higher Psychological Processes. Harvard University Press, Cambridge (1978)

30.

Whalley, J., Kasto, N.: A qualitative think-aloud study of novice programmers’ code writing strategies. In: Conference on Innovation and Technology in Computer Science Education (2014)

31.

Wood, D., Bruner, J.S., Ross, G.: The role of tutoring in problem solving. J. Child Psychol. Psychiatry 17, 89–100 (1976)Crossref

32.

Wrenn, J., Krishnamurthi, S.: Executable examples for programming problem comprehension. In: SIGCSE International Computing Education Research Conference (2019)

33.

Wrenn, J., Krishnamurthi, S., Fisler, K.: Who tests the testers? In: SIGCSE International Computing Education Research Conference, pp. 51–59 (2018)

34.

Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference on Artificial Intelligence (1995)

© Springer Nature Switzerland AG 2019

M. H. ter Beek et al. (eds.)Formal Methods – The Next 30 YearsLecture Notes in Computer Science11800https://doi.org/10.1007/978-3-030-30942-8_2

Successes in Deployed Verified Software (and Insights on Key Social Factors)

June Andronick¹  

(1)

CSIRO’s Data61 and UNSW, Sydney, Australia

June Andronick

Email: june.andronick@data61.csiro.au

Abstract

In this talk, we will share our experience in the successful deployment of verified software in a wide range of application domains, and, importantly, our insights on the key factors enabling such successful deployment, in particular the importance of the social aspects of a group working effectively together.

Our formally verified microkernel, seL4, is now used across the world in a number of applications that keeps growing. Our experience is that such an uptake is enabled not only by a technical strategy, but also by a tight integration of people from multiple disciplines and with both research and engineering profiles. This requires a strong social culture, with well designed processes, for working as one unified team. We share our observations on what concrete social structures have been key for us in creating real-world impact from research breakthroughs.

1 The Dream

Precisely fifty years ago, Tony Hoare, in his seminal paper [1], outlined a dream; a dream where verifying properties of programs can be achieved by purely deductive reasoning; a dream where such reasoning could be applied to non-trivial programs as long as considerably more powerful proof techniques became available; a dream where software systems would not be deployed unless they were formally verified; a dream where verified software would have become the standard produced by industry; a dream where it would be legally considered negligence to deploy unverified software.

We share this dream, and –with many others– have contributed towards it by demonstrating that verified software is feasible and can be deployed on real-world systems. We can, however, observe that, in fifty years, this dream has not been fully achieved yet.

The main reason for verified software not yet being the standard could be phrased as: it has not yet achieved the status of being the state-of-the-art. Ten years ago, Hoare was invited to write a retrospective article [2], to share his personal views on progress made since his first article forty years before, and reflect on what he had hoped for back then and what actually happened. One thing he realised he had not predicted correctly was what actually would drive the push for more verified software; he had thought that it would be the fear of expensive lawsuits for damages due to software errors. This didn’t happen because the defense of ‘state-of-the-art’ practice would always prevail.

We thus need to make verified software become the state-of-the-art practice. For this we need (a) to lower the cost (Hoare said Far more effective is the incentive of reduction in cost [2]) and (b) to have more success stories, where insights can be shared. Together, these will not only bring economic incentives for all software producers to follow the path of verified software, but lead to ‘no more excuses’ not to follow that path.

Here we share our observations about the social structures and incentives that have allowed us to bring together a large group of people with diverse –sometimes even disjoint– technical backgrounds and to make them work effectively towards a goal that must blend relentlessly formal techniques on the one hand with uncompromising real-world performance on the other. In the last ten years, we have been designing, developing, maintaining, and evolving the world’s largest and most verified artefact, ported across multiple hardware platforms, as well as a collection of tools and frameworks for the verification of real-world software. In the last five years, our technology has seen an increasing uptake by companies, governments and the open-source community. This has encouraged a number of initiatives and projects pushing further this pervasive verified software dream. Reflecting on our own experience of what made it possible to push the boundaries of the state-of-the-art into deployed systems, our main insight would be (1) having a single group with both researchers and engineers, and both operating-system (OS) and formal method (FM) experts, all working very closely together, towards a shared vision, and (2) having this vision being not only technical, but also social: making sure this diverse range of people work effectively and efficiently together. We will first give an overview of where our verified software is deployed and the key steps leading to this uptake, and then share our observations on the key social factors that allowed these successes.

2 Successes in Deployed Verified Software

Our story of successfully pushing verified software in deployed systems across a variety of domains contains a few important milestones.

Performance. The first milestone, and starting point, was the research breakthrough making formal program verification scale to an entire operating system kernel, while maintaining high performance. This consisted in the formal proof, in the Isabelle/HOL theorem prover [7], of the functional correctness of the seL4 microkernel [3, 5], followed by the proof of the security properties of integrity [9] and confidentiality [6] as well as correctness of the binary code [8]. Note that the focus on performance as an equal objective as the correctness was a key factor in the later uptake and deployment; and this was made possible only by the close collaboration between the two disciplines’ experts, as we will describe in the next section.

Retrofitting. A second key milestone was to move this research outcome towards a technology transfer in industry by demonstrating the practicality of building whole secure systems on the seL4 trustworthy foundation. We worked with companies to retrofit their existing systems into secure architectures, with isolated trusted components, running on seL4 guaranteeing the isolation (as describes in [4]). The key effort that created the most impact was the High-Assurance Cyber Military Systems (HACMS) program, funded by the US Defense Advanced Research Projects Agency (DARPA), where we collaborated with Boeing, Rockwell Collins, Galois, HRL, the University of Minnesota, MIT, University of Illinois, CMU, Princeton University, and US Army’s TARDEC to transition the seL4 technology to real-world autonomous vehicles. These included a Boeing-built optionally piloted helicopter and an autonomous US-Army truck, both originally vulnerable to cyber-attack, that we demonstrated to be able to resist these cyber-attacks and others after being re-architected to run on seL4. This kind of work is mainly engineering focused, with a join effort between the systems engineers and the proof engineers, keeping the focus on formal guarantees for the security of the overall system. Such projects are also an important source of input about the real-world requirements that need to be addressed.

Focus on Grand Challenges. This leads to the third key ingredient: keep tackling the grand challenges not yet addressed. Our engineering work, pushing our technology on deployed systems, harvests further requirements calling for still more research advances, such as extending the verification guarantees to timing protection, or concurrent execution on multicore platforms, or increasing the cost-effectiveness of verifying application code or porting the proofs to new platforms. These open questions then constitute our research agenda and roadmap.

Open Source. Finally, the last key contributing factor to the uptake of our technology was the open-sourcing of seL4, both code and proofs, as well as all the infrastructure, tools, and platforms to help building whole secure systems. The first reason why this contributed to the uptake is that a kernel is only a part of the solution, and transitioning to using it requires a retrofit, a re-architecting of an existing system, which is not a decision taken lightly. Being able to explore and ‘play’ with it before ‘buying into it’ has been instrumental to people choosing to transition. The second reason open sourcing has been critical is that it builds a community and an ecosystem supporting and extending the technology, infrastructure, libraries, and platforms, helping with the scalability of the support for transitioning. The caveat and challenge is to ensure that the verification guarantees keep being maintained.

These few key milestones have led to an increased uptake of the seL4 kernel and associated technology in real-world systems across a number of domains: automotive (e.g. HRL, TARDEC), aviation (e.g. Boeing, Rockwell), space (e.g. UNSW QB50), military (e.g. Rockwell Soldier Helmet), data distribution (e.g. RTI Connext DDS Micro), Industry 4.0 (e.g. HENSOLDT Cyber), component OS (e.g. Genode platform), security (e.g. Penten Altrocrypt). Some of these projects are a result of DARPA’s call for specific funding to build the seL4 ecosystem, through a number of Small Business Innovation Research (SBIR) grants.

Much work is still to be done (and is ongoing) to lower the bar to transition to seL4-based systems, and to ensure the verification guarantees are maintained and extended, but these successful deployments are contributing to pushing the dream of verified software becoming the default.

3 Insights on Key Social Factors

A major aspect of what we want to communicate here is the importance of social factors, within our group¹, that we have discovered are key contributors to the technical aspects of what we have done. Our experience is that the successful uptake of our technology comes from having a single group hosting both FM and OS people, and both researchers and engineers, working effectively together, as a tightly integrated team. We want to share concrete examples of the social structures that enabled this tight integration for us. Some can be expected and are not unique to our group; we here simply share which ones seem to have been key for us.

Achieving the dream of pervasive verified software requires a combination of academic research and industrial engineering. Today, these mostly live in separated worlds. Industrial engineering brings the real-world requirements, requires usability and performance, but is product-focused and aims at profitability. Hoare said The goal of industrial research is (and should always be) to pluck the ‘low-hanging fruit’; that is, to solve the easiest parts of the most prevalent problems, in the particular circumstances of here and now. [2]. Academic research, on the other hand, is innovation-focused, aiming at generic solutions, with a timeframe allowing grand-challenges to be solved in a novel way. Hoare said that the goal of the pure research scientist is exactly the opposite: it is to construct the most general theories, covering the widest possible range of phenomena, and to seek certainty of knowledge that will endure for future generations. [2]. When it comes to verified software, academic research is still crucially needed to increase the scalability and applicability, while industrial engineering is critical to produce specific instances that work.

There have been many studies on the barriers to the adoption of formal methods and the ideas for closing the gaps between academic research and industry practices. These studies paint the world as composed of two separate entities; the formal methods on one side, and the application domain on the other; or the research on one side, and the industrial engineering on the other — with a boundary in between that needs to be crossed, as a ‘baton’ transferred from one part of the world to the other.

Our view is that success in deployable verified software comes with having one single world, one single team², tighly integrated. It is the notion of tight integration that is crucial. That is what prevents the (undesirable) re-creation, within the group, of the binary world we are presently forced to inhabit outside it. If we don’t succeed there, then the same boundaries and gaps will be created — where work is ‘handed over’ by one set of people to another set of people for their consideration. Instead, people need to work hand in hand, day by day, sometimes even hour by hour, sharing their perspective of the issues, solutions, design decisions, all along the way.

In our group, this is illustrated by the fact that ‘every project involves every subteam’, meaning that the majority of our projects involve both OS and FM people and both researchers and engineers. Our engineering practices and processes on the OS side and FM side are also tightly integrated; for instance, any change in the code, from any side, starts with a discussion on the implications for the ‘other side’; we have a continuous integration process that manages our implementation code base as well as all our proof code base (now more than a million lines of Isabelle/HOL), making sure they are always in sync, that changes to code that is not yet verified can be seamlessly integrated, as well as changes to verified code that happen to not break any proofs, whereas any changes that break the proofs are clearly marked as such and follow a process where a team is allocated to their verification and changes cannot be integrated until the proofs are re-established.

For this tight integration to work, the frequency of the personal interactions is crucial. Our group has experienced a few different physical setups, in different locations, and our observation is that having people in the same location, same building, if possible same floor is highly desirable: a proof engineer can just walk up to the OS engineer to check e.g. whether a change in the code to ease verification would have a performance impact; the impromptu encounters at the coffee machine create the opportunity to share a viewpoint on e.g. a desired kernel change; the kind of discussions needed across disciplines work best as face-to-face discussions, with the support of a white board for design brainstorming, or for sharing the knowledge between disciplines.

Another very important social aspect is ensuring good communication despite the difference in backgrounds, or even sometimes languages and terminologies. For instance, like many other groups, we run weekly talks and quarterly dive-ins to update the rest of the group on progress in various project or share knowledge in a specific area. Maybe unlike many other research groups, these talks cross discipline boundaries and we strive –and in fact need– to keep them at a level all can understand i.e. the OS-based talks have to be FM-comprehensible, and vice versa. And everyone must give one of these talks, on a regular schedule. This way everyone get the opportunity to share their views, to attract interest in their work, and to grow their skills in explaining their work. This fosters a culture inside the group of knowledge sharing and awareness of other people’s work, which is essential when having to then deliver together on a given project. Being able to effectively communicate technical work to people outside of the field is not easy. To help with this, we run annual ‘bootcamps’ focusing on training ourselves on communication and presentation skills, and learning how to best adapt to various kinds of audience. This has an important direct impact on getting traction externally to increase the uptake of our technology, and verified software in general. Importantly, it also enables the needed information sharing and productive collaboration within the group.

Creating a one-team culture goes beyond the communication aspect. It requires a technical vision that everyone shares, shapes and contributes to. But it also needs a culture of achieving this vision together as a team, where we have the urge to see each other succeed, where we help and support each other in solving hard problems and delivering on projects, and where everyone contributes to creating an environment where everyone can thrive. One way this is achieved in our group is that a lot of activities such as trainings, social events, or cultural awareness initiatives are done by people from the group, and tailored to what our groups needs. For instance, our bootcamp mentioned above includes sessions on active listening, mental health, life balance, and all sessions are given by members of the group that have either training or first-hand experience in the topic, and are delivering tailored information and practice that they know are relevant to the type of work we do. The impact of this approach is that the trust that people have in their peers amplifies the impact of the message, the learning experience or the social interaction. It also extends the scope of the collaboration between people from purely technical to all social aspects of the group’s life.

All of the above creates and fosters an environment where you can get a unique combination of people with different expertise and profiles that can work well together to achieve their shared mission. Dealing with a truly wonderful mix of personalities, backgrounds and cultures does create a number of challenges, but it also creates the required structure to tackle and solve research grand challenges, while producing systems, tools and frameworks that the world can use and deploy, and while building a community of users, partners and contributors. And this is what is needed to achieve the dream of shifting the whole world’s mentality towards accepting verified software as the norm.

Acknowledgements

The author would like to thank Gerwin Klein and Carroll Morgan for their feedback on drafts of this paper.

References

1.

Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576–580 (1969)Crossref

2.

Hoare, C.A.R.: Viewpoint - retrospective: an axiomatic basis for computer programming. CACM 52(10), 30–32 (2009)Crossref

3.

Klein, G., et al.: seL4: Formal verification of an operating-system kernel. CACM 53(6), 107–115 (2010)Crossref

4.

Klein, G., Andronick, J., Kuz, I., Murray, T., Heiser, G., Fernandez, M.: Formally verified software in the real world. CACM 61, 68–77 (2018)Crossref

5.

Klein, G., et al.: seL4: Formal verification of an OS kernel. In: SOSP, pp. 207–220. ACM, Big Sky, October 2009

6.

Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, pp. 415–429. IEEE, San Francisco, May 2013

7.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://​doi.​org/​10.​1007/​3-540-45949-9CrossrefzbMATH

8.

Sewell, T., Myreen, M., Klein, G.: Translation validation for a verified OS kernel. In: PLDI, pp. 471–481. ACM, Seattle, June 2013

9.

Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 325–340. Springer, Heidelberg (2011). https://​doi.​org/​10.​1007/​978-3-642-22863-6_​24Crossref

Footnotes

1

the Trustworthy Systems group, in Data61, CSIRO, https://​ts.​data61.​csiro.​au.

2

and if possible, importantly, one single shared coffee machine, surrounded by plenty of whiteboards.

Verification

© Springer Nature Switzerland AG 2019

M. H. ter Beek et al. (eds.)Formal Methods – The Next 30 YearsLecture Notes in Computer Science11800https://doi.org/10.1007/978-3-030-30942-8_3

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm

Mariano M. Moscato¹  , Laura Titolo¹  , Marco A. Feliú¹   and César A. Muñoz²  

(1)

National Institute of Aerospace, Hampton, USA

(2)

NASA Langley Research Center, Hampton, USA

Mariano M. Moscato (Corresponding author)

Email: mariano.moscato@nianet.org

Laura Titolo

Email: laura.titolo@nianet.org

Marco A. Feliú

Email: marco.feliu@nianet.org

César A. Muñoz (Corresponding author)

Email: cesar.a.munoz@nasa.gov

Abstract

The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating-point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in-polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source-to-source transformation of the ideal real-number specification of the algorithm. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).

Research by the first three authors was supported by the National Aeronautics and Space Administration under NASA/NIA Cooperative Agreement NNL09AA00A.

1 Introduction

PolyCARP (Algorithms for Computations with Polygons) [25, 27] is a NASA developed open source software library for geo-containment applications based on polygons.¹ One of the main applications of PolyCARP is to provide geofencing capabilities to unmanned aerial vehicles (UAV), i.e., detecting whether a UAV is inside or outside a given geographical region, which is modeled using a 2D polygon with a minimum and a maximum altitude. Another application is detecting if an aircraft’s trajectory encounters weather cells, which are modeled as moving polygons.

PolyCARP implements point-in-polygon methods, i.e., methods for checking whether or not a point lies inside a polygon, that are based on the winding number computation. The winding number of a point p with respect to a polygon is the number of times any point traveling counterclockwise along the perimeter of the polygon winds around p. Properties of these methods have been formally verified in the Prototype Verification System (PVS) [28]. A correct implementation of these methods is essential to safety-critical geo-containment applications that rely on PolyCARP.

When an algorithm involving real numbers is implemented using floating-point numbers, round-off errors arising from the difference between real-number computations and their floating-point counterparts may affect the correctness of the algorithm. In fact, floating-point implementations of point-in-polygon methods are very sensitive to round-off errors. For instance, the presence of floating-point computations in Boolean expressions of conditional statements may cause the control flow of the floating-point program to diverge from the ideal real-number program, resulting in the wrong computation of the winding number. This may happen even when the point is far from the edges of the polygon.

This paper presents a formally verified floating-point C implementation of the winding number algorithm. This implementation is obtained by applying a program transformation to the original algorithm. This transformation replaces numerically unstable conditions with more restrictive ones that preserve the control flow of the ideal real number specification. The transformed program is guaranteed to return a warning when real and floating-point flows may diverge. The program transformation used is an extension of the one defined in [32] and it has been implemented within PRECiSA² (Program Round-off Error Certifier via Static Analysis), a static analyzer of floating-point programs [24, 30].

Frama-C [20] is used to formally verify the correctness of the generated C program. Frama-C is a collaborative platform that hosts several plugins for the verification and analysis of C code. In particular, in this work, an extension of the Frama-C/WP (Weakest Precondition calculus) plugin is implemented to automatically generate verification conditions that can be discharged in PVS.

The rest of this paper is organized as follows. Section 2 presents the definition of the winding number. An extension of the program transformation defined in [30] is presented in Sect. 3. In Sect. 4, the transformed floating-point version of the winding number is introduced. The verification approach used to prove the correctness of the C floating-point implementation of the transformed program is explained in Sect. 5. Related work is discussed in Sect. 6. Finally, Sect. 7 concludes the paper.

2 The Winding Number Algorithm

The winding number of a point s with respect to a polygon P is defined as the number of times the perimeter of P travels counterclockwise around s. For simple polygons, i.e., the ones that do not contain intersecting edges, this function can be used to determine whether s is inside or outside P. In [25], the winding number of s with respect to P is computed by applying a geometric translation that sets s as the origin of coordinates. For each edge e of P, the algorithm counts how many axes e intersects. This contribution can be positive or negative, depending on the direction of the edge e. If the sum of all contributions from all edges is 0 then s is outside the perimeter of P, otherwise, it is inside. Figure 1 shows the edge contributions in the computation of the winding number for two different polygons.

Fig. 1.

Winding number edge contributions

Mathematical functions that define the winding number algorithm are presented in Fig. 2. Given a point

, the function

returns the quadrant in which v is located. Given the endpoints of an edge e,

and

, and the point under test

, the function

computes the number of axes e intersects in the coordinate system centered in s. This function checks in which quadrants v and $$v'$$ are located and counts how many axes are crossed by the edge e. If v and $$v'$$ belong to the same quadrant, the contribution of the edge to the winding number is 0 since no axis is crossed. If v and $$v'$$ lie in adjacent quadrants, the contribution is 1 (respectively -1) if moving from v to $$v'$$ along the edge is in counterclockwise (respectively clockwise) direction. In the case v and $$v'$$ are in opposite quadrants, the determinant is computed to check the direction of the edge. If it is counterclockwise, the contribution is 2; otherwise, it is -2. The function

takes as input a point

and a polygon P of size n, which is represented as a couple of arrays $$\langle P_x,P_y \rangle $$ modeling the coordinates of its vertices

. The size of a polygon is defined as the number of its vertices. The winding number of s with respect to the polygon P is obtained as the sum of the contributions of all the edges in P. The result of the winding number is 0 if and only if the polygon P does not wind around the point s, hence s lies outside P.

Fig. 2.

Winding number algorithm

It has been formally verified in PVS, that the algorithm presented in Fig. 2 is equivalent to an alternative point-in-polygon algorithm.³ The following property is therefore assumed.

Property 1

Given a simple polygon

and a point

, s lies outside P if and only if

.

A formal proof of Property 1 that does not rely on an alternative algorithmic method to check point containment is a hard problem beyond the scope of this paper. In particular, a proof of this statement involving a non-algorithmic definition of containment may require the formal development of fundamental topological concepts such as the Jordan Curve theorem.

3 Program Transformation to Avoid Unstable Tests

Floating-point numbers are widely used to represent real numbers in computer programs since they offer a good trade-off between efficiency and precision. A floating-point number can be formalized as a pair of integers

, where m is called the significand and $$ e _{}$$ the exponent of the float [7, 13]. Henceforth, $$\mathbb {F}$$ will denote the set of floating-point numbers. A conversion function ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq22_HTML.gif is defined to refer to the real number represented by a given float, i.e., ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq23_HTML.gif where b is the base of the representation. According to the IEEE-754 standard [19], each floating-point operation must be computed as if its result is first calculated correct to infinite precision and with unbounded range and then rounded to fit a particular floating-point format.

The main drawback of using floating-point numbers is the presence of round-off errors that originate from the difference between the ideal computation in real arithmetic and the actual floating-point computation. Let ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq24_HTML.gif be a floating-point number that represents a real number ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq25_HTML.gif , the difference ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq26_HTML.gif is called the round-off error (or rounding error) of ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq27_HTML.gif with respect to ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq28_HTML.gif . Rounding errors accumulate during the program execution and may affect the evaluation of both arithmetic and Boolean expressions. As a consequence, when guards of if-then-else statements contain floating-point expressions, as in the case of the winding number, the output of a program is not only directly influenced by rounding errors, but also by the error of taking the opposite branch with respect to the real number intended behavior. This problem is known as test instability. A conditional statement (or test)

is said to be unstable when $$\tilde{\phi }$$ evaluates to a different Boolean value than its real-valued counterpart.

In [32], a formally proven⁴ program transformation is proposed to detect and correct the effects of unstable tests for a simple language with conditionals and let-in expressions. The output of the transformation is a floating-point program that is guaranteed to return either the result of the original floating-point one, when it can be assured that both the real and its floating-point flows agree, or a warning, when these flows may diverge. In this paper, the transformation defined in [32] has been extended to handle non-recursive function calls and simple for-loops. This extended transformation is then applied to the winding number algorithm.

Henceforth, the symbols $$\mathbb {A}$$ and $$\widetilde{\mathbb {A}}$$ denote the domain of arithmetic expressions over real and floating-point numbers, respectively. It is assumed that there is a function ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq33_HTML.gif that associates to each floating-point variable $$\tilde{x}$$ a variable $$x \in \mathbb {V}$$ representing the real value of $$\tilde{x}$$ . The function ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq37_HTML.gif converts an arithmetic expression on floating-point numbers to an arithmetic expression on real numbers. This function is defined by simply replacing each floating-point operation with the corresponding one on real numbers and by applying $$ R $$ and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq39_HTML.gif to floating-point values and variables, respectively. By abuse of notation, floating-point expressions are interpreted as their real number evaluation when occurring inside a real-valued expression. The symbols $$\mathbb {B}$$ and $$\widetilde{\mathbb {B}}$$ denote the domain of Boolean expressions over real and floating-point numbers, respectively. The function ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq42_HTML.gif converts a Boolean expression on floating-point numbers to a Boolean expression on real numbers. Given a variable assignment

,

denotes the evaluation of the real Boolean expression B. Similarly, given $$\widetilde{B}\in \widetilde{\mathbb {B}}$$ and

,

denotes the evaluation of the floating-point Boolean expression $$\widetilde{B}$$ . A program is defined as a set of function declarations of the form

, where $$ S $$ is a program expression that can contain binary and n-ary conditionals, let expressions, arithmetic expressions, non-recursive function calls, for-loops, and a warning exceptional statement $$\omega $$ . Given a set $$\varSigma $$ of function symbols, the syntax of program expressions $$ S $$ is given by the following grammar.

(3.1)

where $$\widetilde{ A }\in \widetilde{\mathbb {A}}$$ , $$\widetilde{ B }\in \widetilde{\mathbb {B}}$$ ,

, $$g \in \varSigma $$ , $$m\in \mathbb {N}^{>0}$$ , and

. The notation

denotes a list of m $$\mathrel { elsif }$$ branches. The ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq62_HTML.gif expression emulates a for loop where i is the control variable that ranges from $$i_{0}$$ to $$i_{n}$$ , $$ acc $$ is the variable where the result is accumulated with initial value $$ acc _{0}$$ , and S is the body of the loop. For instance, ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq67_HTML.gif represents the value f(1, 0), where f is the recursive function

. The set of program expressions is denoted as $$\mathbb {S}$$ , while the set of programs is denoted as $$\mathbb {P}$$ .

The proposed transformation takes into account round-off errors by replacing the Boolean expressions in the guards of the original program with more restrictive ones. This is done by means of two abstractions ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq71_HTML.gif defined as follows for conjunctions and disjunctions of sign tests, where $$\widetilde{ expr }\in \widetilde{\mathbb {A}}$$ and $$\epsilon \in \widetilde{\mathbb {V}}$$ is a variable that represents the rounding error of $$\widetilde{ expr }$$ such that ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq75_HTML.gif and $$\epsilon \ge 0$$ .

Generic inequalities of the form $$a<b$$ are handled by replacing them with their equivalent sign-test form $$a-b<0$$ .

The following lemma states that ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq79_HTML.gif implies both $$\tilde{\phi }$$ and its real counterpart, while ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq81_HTML.gif implies both the negation of $$\tilde{\phi }$$ and the negation of its real counterpart. The proof is available as part of the PVS formalization defined in [32].

Lemma 1

Given $$\tilde{\phi }\in \widetilde{ B }$$ , let ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq84_HTML.gif be the set of free variables in $$\tilde{\phi }$$ . For all ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq86_HTML.gif , ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq87_HTML.gif , and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq88_HTML.gif such that ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq89_HTML.gif , ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq90_HTML.gif and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq91_HTML.gif satisfy the following properties.

1.

.

2.

.

The transformation function ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq94_HTML.gif and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq95_HTML.gif to the guards in the conditionals. For binary conditional statements, ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq96_HTML.gif is defined as follows.

If ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq97_HTML.gif or ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq98_HTML.gif :

If ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq99_HTML.gif and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq100_HTML.gif :

When the round-off error does not affect the evaluation of the Boolean expression, i.e., ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq101_HTML.gif and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq102_HTML.gif , the transformation is just applied to the subprograms $$S_1$$ and $$S_2$$ . Otherwise, the then branch of the transformed program is taken when ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq105_HTML.gif is satisfied. From Lemma 1, it follows that both $$\tilde{\phi }$$ and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq107_HTML.gif hold and, thus, the then branch is taken in both real and floating-point control flows. Similarly, the else branch of the transformed program is taken when ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq108_HTML.gif holds. This means that in the original program the else branch is taken in both real and floating-point control flows. When neither ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq109_HTML.gif nor ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq110_HTML.gif is satisfied, a warning $$\omega $$ is issued indicating that floating-point and real flows may diverge. In the case of the for-loop, the transformation is applied to the body of the loop.

(3.2)

Given a program $$P\in \mathbb {P}$$ , the transformation ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq113_HTML.gif is defined as follows.

(3.3)

where ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq114_HTML.gif is applied to the body of the function and new arguments $$e_1,\dots ,e_m$$ are added to represent the round-off error of the arithmetic expressions occurring in each test in the body of S. When either ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq116_HTML.gif or ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq117_HTML.gif is applied to a test in S, e.g. $$\widetilde{ expr }< 0$$ , a new fresh variable $$e$$ is introduced representing the round-off error of the arithmetic expression occurring in the test. This fresh variable becomes a new argument of the function and a pre-condition is imposed stating that ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq120_HTML.gif . In addition, for every function call

occurring in S, the error variables of g, $$e'_1,\dots ,e'_k$$ , are added as additional arguments to f.

When a function g is called, it is necessary to check if the returning value is a warning $$\omega $$ . Let

be a call to the function

in the original program with actual parameters

. Additionally, let ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq127_HTML.gif be the corresponding function declaration in the transformed program such that for all

, $$\widetilde{ expr }_i$$ is an arithmetic expression occurring in a transformed test and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq130_HTML.gif . The transformation of the function call is defined as follows:

where for all

, $$e'_i$$ is such that

. In this case, the information regarding the error variables is instantiated with the actual parameters of the function.

The following theorem states the correctness of the program transformation. The transformed program is guaranteed to return either the result of the original floating-point program, when it can be assured that both its real and floating-point flows agree, or a warning $$\omega $$ when these flows may diverge.

Theorem 1

(Program Transformation Correctness). Given ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq135_HTML.gif , for all ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq136_HTML.gif , ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq137_HTML.gif , and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq138_HTML.gif , such that for all ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq139_HTML.gif , ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq140_HTML.gif :

where ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq141_HTML.gif .

Theorem 1 follows from Lemma 1 and the definition of the program transformation ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq142_HTML.gif . It has been formally proved in PVS for the particular case of the winding number transformation. A general PVS proof of this statement for an arbitrary program is under development.

4 Test-Stable Version of the Winding Number

The use of floating-point numbers to represent real values introduces test instability in the program defined in Sect. 2. A technique used in PolyCARP to mitigate the uncertainty of floating-point computations in the winding number algorithm is to consider a buffer area around the perimeter of the polygon that is assumed to contain the points that may produce instability. As part of this work, the PRECiSA static analyzer [24, 30] is used to validate if a buffer that protects against instability exists. PRECiSA accepts as input a floating-point program and computes a sound over-approximation of the floating-point accumulated round-off error that may occur in each computational path of the program. In addition, the corresponding path conditions are also collected for both stable and unstable cases. When real and floating-point flows diverge, PRECiSA outputs the Boolean conditions under which the instability occurs.

Given the unstable conditions produced by PRECiSA for the winding number algorithm, an over-approximation of the region of instability is generated by using the paving functionality of the Kodiak global optimizer [26]. Concrete examples for these instability conditions are searched in the instability region by using the FPRoCK [29] solver, a tool able to check the satisfiability of mixed real and floating-point Boolean expressions. As an example, consider the edge $$(v,v')$$ , where $$v=(1,1)$$ and

, in the polygon depicted in Fig. 3. The red lines represent a guaranteed over-approximation of the values for $$s_x$$ and $$s_y$$ that may cause instability in the function

with respect to the considered edge. The black aircraft denotes a case in which the contribution of the edge $$(v,v')$$ has a different value in real and floating-point arithmetic. In fact, when $$s_x = 4$$ and

, the real function

returns -1, indicating that v and $$v'$$ are located in adjacent quadrants. However, its floating-point counterpart returns 0 meaning that the vertices are located in the same quadrant. The red aircraft represents the point

, $$s_y = 1.5$$ , for which the main function

returns 0, i.e., the point is outside, when evaluated with real arithmetics, and it returns 4, i.e., the point is inside, when evaluated in floating-point arithmetic. This figure suggests that simply considering a buffer around the edge is not enough to guarantee the correct behavior of the

function since errors in the contribution can happen also when the point is far from the boundaries. It has been conjectured that, for this algorithm, when the checked point is far from the edges of the polygon, the error occurring in one edge is compensated with the error of another edge of the polygon in the computation of the winding number. To the authors’ knowledge, no formal proof of this statement exists.

Fig. 3.

Points that cause instability in

and

.

The floating-point program depicted in Fig. 4 is obtained by applying the transformation ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq160_HTML.gif from Sect. 3 to the real-number winding number algorithm presented in Fig. 2. The function

has two additional arguments, $$e_x$$ and $$e_y$$ , modeling the round-off errors of $$v_x$$ and $$v_y$$ , respectively. Thus,

(4.1)

The tests are approximated by means of the functions ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq166_HTML.gif and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq167_HTML.gif by replacing the value 0 with the error variables $$e_x$$ and $$e_y$$ .

The function

contains two calls to

. Therefore, it is necessary to check if any of these calls return a warning $$\omega $$ . If this is the case,

also returns $$\omega $$ since a potential instability has been detected in the calculation of

. The function

has five additional arguments with respect to its real number counterpart

. Besides $$e_{ det }$$ that represents the error of the expression calculating the determinant, the error variables appearing in the calls to

are considered: ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq180_HTML.gif , ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq181_HTML.gif , and ../images/478451_1_En_3_Chapter/478451_1_En_3_IEq182_HTML.gif . The new parameters are such that:

(4.2)

The conditional in the main function

does not introduce any new error variable, therefore just the error parameters in the calls to

are considered. Let

be the size of the polygon P, and let $$ fdet $$ be the function calculating the determinant, which is defined as follows

(4.3)

The error variables $$e_{x}$$ , $$e_{y}$$ , and $$e_{ det }$$ are such that:

(4.4)

5 Verification Approach

This section presents the approach used to obtain a formally verified test-stable C implementation of the winding number algorithm that uses floating-point numbers. The toolchain is comprised of the PVS interactive prover, the static analyzer PRECiSA, and the Frama-C analyzer [20]. The input is a real-valued program P expressed in the PVS specification language. The output is a C implementation of P that correctly detects and corrects unstable tests. An overview of the approach is depicted in Fig. 5.

Fig. 4.

Pseudo-code on floating-point arithmetic of the transformed winding number algorithm

Fig. 5.

Verification approach.

As already mentioned, PRECiSA is a static analyzer that computes an over-estimation of the round-off error that may occur in a program. In addition, it automatically generates a PVS proof certificate ensuring the correctness of the computed bound. In this work, PRECiSA is extended to implement the transformation defined in Sect. 3 and to generate the corresponding C code. Given a desired floating-point format (single or double precision), PRECiSA is used to convert the PVS real-number version of the winding-number algorithm defined in