Trace: • schedule

Table of Contents

The complete schedule is found on BYU Learning Suite; though a tentative reading schedule is provided below for review.

Fall 2018

Create a verification tool for a simple restricted language that is able to:

  • Static Check the program for type safety and that all variables are declared
  • Simulate the language prompting the user if ever there is a non-deterministic choice
  • Model Check simple linear temporal logic properties
  • Automatically generate tests for branch coverage
  • Abstract Interpret over simple abstractions for safety properties

The language can use any syntax and minimally must support

  • Primitive types: char, int, and string (signed only)
  • Output to the console
  • Function calls with parameters, local variables, and single scope
  • Operators for integer linear arithmetic (plus, minus, and limited multiplication).
  • Standard relational operators: less-than, less-than-equal, equal, etc.
  • Logical operators: not, and, or
  • if-then-else statements
  • while statements
  • return statements
  • non-determistic input so that input can be defined over a range of values
  • Extra: a keyword to create threads of execution

Parsing

Please using any tool for the parsing. Write the grammar in whatever textural form is used by the tool being used to generate the parser. Here is an example of a Static Java language described for the ANTLR tool. It has a super set of the required language properties.

If you are using an LL(n) parser then left-factoring and removing left recursion in the grammar will be important:

The output of the parser should be an abstract syntax tree. Any language may be used to implement that tree (and the verification tool for that matter). It is highly recommended to use a visitor pattern with the abstract syntax tree.

Note that one of the compiler passes will be to transform the language into A-normal form. Here is the Wiki version for A-normal Form. You may define other passes to simplify simulation as desired.

Here is a git repository with resources on ANTLR (see lectures/ANTLR-tutorial-calc 

git clone ssh://@schizo.cs.byu.edu/~egm/public-git/cs431/lectures

There are also several lectures on the visitor pattern, symbol tables, and type checking.

Static Check

The tool should build a symbol table as a pass on the AST. That table should include functions and variables and ensure that only declared things or used. In a second pass, it should construct a type proof showing that all statements are type correct.

Simulation

Simulation is based on the CESK framework. A lighter read is Java as a CESK machine.

A CESK machine defines state to consist of a control, environment, a store, and a continuation. It is a powerful model for semantics capable of handling all the complexity of higher-order languages. Although the language here is not high-order, the CESK model is a clean and convenient way to define the semantics of the language and give those semantics operational capabilities. Indeed, one of the strengths of CESK is that the semantic definition is operational.

Semantics are defined by rules that govern transitions between states. Each rule defines the conditions that must hold in the source state with the conditions that must hold in the target state. The rules clearly define how the source state is related to the target state.

Model Checking

We are interested in model checking via automata theory. The basis is in language intersection where the model of the system forms one language and the property forms another language. The property is complemented and then the two languages, the model and complemented property, are intersected to see in there are any common words in the intersection. A word in the intersection is a counter example.

There are two free online sources to study to learn the algorithms. The first is Principles of Model Checking Chapter 4. First study how to intersect NFAs, and then study sections 4.2 and 4.3 to apply it to infinite words on Buchi Automata. The infinite words capture liveness properties.

The second online source is Model Checking Chapter 9. This book is available, in electronic form, through the Harold B. Lee Library. Click on Books on the left sidebar. Search for Model Checking, and then follow the links to the electronic version. Here are the key topics that you need to understand:

  • Buchi automaton and infinite words
  • Intersecting Buchi automaton with the simplified algorithm where all states are accepting in one automaton
  • Double depth-first search for cycle detection
  • On-the-fly model checking
  • Converting a Kripke structure or labeled transition system to an automaton

The project is to first introduce a key-word into the language, select (i : 1 .. N), for non-determinism. The meaning of the new key-word is to non-deterministically chooses a value for i from the range.

Second, create an API to be able to hard-code a property automaton in the code, and then use it to intersect with the program under verification reporting the counter-example if one exists.

Symbolic Execution for Source Code Verification

Use symbolic execution to verify a use indicated function in the program. To support the verification, add to the language two statements:

  • assume: takes a predicate on a variable and restricts that variable to ranges where the predicate is true.
  • assert: takes a predicate on a variable and fails if that predicate is not true.

With the addition of these two statements, it is possible to assume pre-conditions and assert post-conditions for program verification via symbolic execution.

The symbolic execution for this assignment will use path merging to reduce the complexity of the search space. It will also require that the tool interface with an SMT solver.

There are several useful references for the needed background. Here are a few to get started:

The ultimate goal is to implement the path merging version of symbolic execution (the BDDs are a non-needed optimization) for your language, so read the background material enough to understand the approach.

Abstract Interpretation

Fall 2017

Old Schedule

Tools To Consider

Papers for another day

cs-686/schedule.txt · Last modified: 2018/10/23 10:23 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0