http://lara.epfl.ch/web2010/ 2013-05-20T04:11:09+02:00 http://lara.epfl.ch/web2010/ http://lara.epfl.ch/web2010/lib/images/favicon.ico text/html 2013-05-19T20:54:42+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/sav13:lecturecise_21?rev=1368989682&do=diff1368989682 Continuing Lecturecise 20 Finish example for ground and non-ground resolution: [pdf] Effectively Propositional Logic (EPR) and Importance of Finite Herbrand Universe * exists x1,...,xn. forall y1,...,ym. G * only relation symbols and constants allowed * Skolemization gives only constants, so the set of ground terms finite (bounded by number of original constants + existentials) text/html 2013-05-19T20:50:13+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/leon?rev=1368989413&do=diff1368989413 [The One, Leon Way] Leon is an automated system for verifying functional Scala programs, finding counterexamples to the validity of user-specified properties, and synthesizing programs from specifications and examples. The system can be tried out online, with no installation required, at the following link: text/html 2013-05-19T20:49:50+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/start?rev=1368989390&do=diff1368989390 Mission: Help people construct software that does what they expect NEWS and the RSS Feed ---------- LARA develops precise automated reasoning techniques: tools, algorithms, languages. We apply these techniques to synthesis and verification of computer systems. See, for example, the Leon verification and synthesis system. text/html 2013-05-17T22:25:31+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/insynth?rev=1368822331&do=diff1368822331 InSynth is a tool for interactive synthesis of code snippets. It synthesizes a ranked list of code fragments that use given library functions. A recent version is presented in the following paper: * Complete Completion using Types and Weights, PLDI’2013 text/html 2013-05-16T17:59:24+02:00 Mikaël Mayer http://lara.epfl.ch/web2010/pong?rev=1368719964&do=diff1368719964 The increasing adoption of smartphones and tablets has provided tens of millions of users with substantial resources for computation, communication and sensing. The availability of these resources has a huge potential to positively transform our society and empower individuals. Unfortunately, although the number of users has increased dramatically, the number of developers is still limited by the high barrier that existing programming environments impose. More than ever, the number of developers… text/html 2013-05-14T18:23:36+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/sav13:top?rev=1368548616&do=diff1368548616 For Moodle page: click here The course will be similar to SAV 2012 and SAV 2011. (See there for overview as well.) We initially refresh our knowledge of logic and agree on notation, but for a more thorough introduction, in addition to many textbooks, you may wish to check the videos of Introduction to Logic course at Coursera. text/html 2013-05-14T18:17:45+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/sav13:lecturecise_22?rev=1368548265&do=diff1368548265 Insertion into Doubly-Linked List Program Memory as Graph Language with Dynamic Allocation Semantics of Dynamic Object Allocation Semantics of Field Reads and Writes Semantics of Array Manipulations Assertions for Correct Use of Arrays and Heaps text/html 2013-05-13T13:58:03+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/sav13:lecturecise_20?rev=1368446283&do=diff1368446283 [PDF Slides] Resolution Theorem Provers Example of a very good theorem prover: * E prover Our running example in latex: Input in TPTP3 format: fof(axTotal,axiom, ![X]:?[Y]: r(X,Y)). fof(axExtends,axiom, ![X]:![Y]: (r(X,Y) => ![Z]:r(X,f(Y,Z)))). fof(axAlt,axiom, ![X]: (p(X) | p(f(X,a)))). fof(c,conjecture, ![X]:?[Y]: (r(X,Y) & p(Y))). text/html 2013-05-12T21:32:17+02:00 Viktor Kuncak http://lara.epfl.ch/web2010/sav13:correspondoutput.txt?rev=1368387137&do=diff1368387137 # No SinE strategy applied fof(c_0_1, axiom, (![X1]:?[X2]:r(X1,X2)) , file('example.p', axTotal)). fof(c_0_2, axiom, (![X1]:![X2]:(r(X1,X2)=>![X3]:r(X1,f(X2,X3)))) , file('example.p', axExtends)). fof(c_0_3, axiom, (![X1]:(p(X1)|p(f(X1,a)))) , file('example.p', axAlt)). fof(c_0_4, conjecture, (![X1]:?[X2]:(r(X1,X2)&p(X2))) , file('example.p', c)). fof(c_0_5, negated_conjecture, (~(![X1]:?[X2]:(r(X1,X2)&p(X2)))) ,inference(assume_negation, [status(cth)],[c_0_4])). fof(c_0_6, plain, (![X3]:?[X4]:r…