2

I am looking for a discussion of how to convert various programming language constructs to Z3, without limiting the efficiency of the solver.

In particular, is there an algorithm and a set of best-practice rules for converting a function/program expressed in continuation passing style to Z3?

The use context is to use Z3 for implementing a type system for a programming language, so the solution has to be efficient and incremental (e.g. retain previous Z3 ASTs in the Z3 instance).

I am aware of Boogie, but is looking for something more lightweight if it is possible.

Constraining the semantics of the input language somewhat is acceptable, but not so far that it is trivially expressible in SMTLIB.

I am basically looking for a discussion of different strategies that one might consider for various typical language constructs.

Edit: It might be acceptable to have restrictions that make the input language non-turing-complete and only reasonable efficient for smaller program fragments (like functions in a library). E.g. the input language could be a language for writing "statically checked" libraries that is later transpiled down to libraries for an existing dynamic programming language with dynamic runtime asserts where appropriate.

Ola Fosheim Grøstad
  • 259
  • 1
  • 6
  • Your question is a bit open-ended, so you might not get a good answer on here. Z3 supports a push/pop mode that should allow you to build up an AST incrementally. Take a look at these questions: [1](https://stackoverflow.com/questions/16422018/how-incremental-solving-works-in-z3) and [2.](https://stackoverflow.com/questions/13959545/how-to-use-z3-incrementally-and-model-without-propositional-value) Also, I would advise for you is to make sure you encode your problem in a decidable theory. I think this should be possible for a type system. – Douglas B. Staple Jun 29 '16 at 12:55
  • Devising such efficient language feature encodings is a core problem of program verification and various research groups have invested lots of research and engineering effort into finding solutions - I therefore strongly doubt that you will (and in general, can) get "nutshell" answers to your question. Consider using an intermediate verification language such as Boogie, Viper or Why3 (or maybe an existing verification systems such as Dafny, VeriFast or Grasshopper) - this is typically a better idea (e.g. quicker prototyping and earlier initial results) compared to using an SMT solver directly. – Malte Schwerhoff Jun 30 '16 at 06:29
  • Thanks for your comments! I would like to prototype it in Python with Z3, but I am willing to limit the input language to what can reasonably be expressed with Z3. I've added some restrictions on the use scenario in the description. – Ola Fosheim Grøstad Jun 30 '16 at 09:41

0 Answers0