Prototype Introduction

This website describes a tool that accompanies the article "Finding Polynomail Loop Invariants for Probabilistic Programs" by Yijun Feng, Lijun Zhang, David N. Jansen and others.


The Prototype is written in Python 3 with an output of Matlab file (.m). To conduct the Invariant, Matlab version of YALMIP and SeDuMi toolboxes are needed. For YALMIP toolbox, one can find the latest version in For semidefinite programming, we use SeDuMi solver, of which the homepage is

Synthesize quantitative loop invariant

To synthesize an invariant for simple loops in probabilistic programs, one need to create a python file to input details about the program. The format can be seen from our provided example with and needed to be imported. After inputing all the details, one needs to create a Matlab_file class defined in, run the create_file function, and name the output file. Then by executing the output file, one can get an executable Matlab file in the same path as your python file.

variables = []  # the variables should be input as a list, with each variable as a string, and comma as split symbol
pre_exp  = '' # a string for pre_exp
post_exp = '' # a string for post_exp
while_sentence = '' # in the form of 'sentence1[p]sentence2', cannot deal with several sentences yet
while_valuation = [] # a list for the valuation sentence in while loop, each valuation should be written as a string
while_condition = '' # a string denoting while condition, use 'and' or 'or' in the string to denote logical relationship
addition_condition = [] # denoting constraint refinements, each constraint is a string
initial_value = [] # denoting the initial valuation for the loop, each valuatio is a string

Then the class matlab_File is constructed and the function create_file can create the related matlab file.

An interface is also provided to make user input more convenient. The user still needs to input the items mentioned in the table above, but not in the formation of programming language. The following picture shows an example.

"maximum degree of template" can be remained empty and the programme will use a default value. Since we cannot assume a default installation path for Matlab in user's computer, the interface also generates a matlab file that needs the user to execute manually.


Prototype.rar download


All examples download
ruin python matlab
bin1 python matlab
bin2 python matlab
bin3 python matlab
sum python matlab
perceptron python matlab
airplane1 python matlab
airplane2 python matlab
parameterized probilistic program python degree = 4
parameterized ruin python matlab degree = 8 degree = 9

Examples for nested loop programs are also provided here, but not yet supported by our prototype, so only matlab files are presented.

nested loop 1 matlab

Copyright(c) 2017 by Yijun Feng. The tool may only be downloaded, stored temporarily and run by reviewers of the submitted article in their evaluation tast. All other right reserved.
For any questions, feel free to contact