http://www.ocf.berkeley.edu/~rhishi/ 2009-10-29T04:06:06-07:00 http://www.ocf.berkeley.edu/~rhishi/ http://www.ocf.berkeley.edu/~rhishi/lib/images/favicon.ico text/html 2009-10-27T11:12:00-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/smt/lazy?rev=1256667120&do=diff SAT solver. Theory solver (T-solver) that can decide conjunction of literals. A propositional SAT solver uses the following DPLL rules: * Unit-propagate: BCP / unit-propagation. * Pure literal * Decide: choose a value for a variable that is undefined. * Learn: deduce a new clause implied by F. * Backjump: non-chronological backtracking. * Fail: a clause is falsified and there are no more decisions to try. * Forget: drop some implied clauses. * Restart: reset the model and sta… text/html 2009-10-26T09:50:39-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/smt/mcmillan2003interpolation?rev=1256575839&do=diff Symbolic model checking: verifying temporal properties of finite-state (or sometimes infinite-state) systems using symbolic representation of sets of states, e.g. BDDs. This is unbounded model checking, i.e. it's sound as well as complete. Bounded model checking: searching for a counterexample of bounded length using SAT solver. It's sound, but not complete. text/html 2009-10-25T10:58:46-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/smt/mcmillan2005interpolating?rev=1256493526&do=diff Craig interpolant: given an inconsistent pair of logical formulas, (i.e. is unsatisfiable), a Craig interpolant is a formula that is implied by , is inconsistent with , and refers only to uninterpreted symbols common to and . For propositional logic, given a proof of unsatisfiability in the form of resolution steps, interpolant can be derived in linear time. [5] [12]. text/html 2009-10-24T23:25:19-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/autotools/start?rev=1256451919&do=diff ''%%AC_CHECK_PROG (variable, prog-to-check-for, value-if-found, [value-if-not-found], [path = ‘$PATH’], [reject])%%'' ''%%AC_CHECK_PROGS (variable, progs-to-check-for, [value-if-not-found], [path = ‘$PATH’])%%'' ''%%AC_PATH_PROG (variable, prog-to-check-for, [value-if-not-found], [path = ‘$PATH’])%%'' ''%%AC_PATH_PROGS (variable, progs-to-check-for, [value-if-not-found], [path = ‘$PATH’])%%'' $PATH_SEPARATOR # The order is important: first termcap and then readline. AC_SEARCH_LIBS([tgeten… text/html 2009-10-19T14:58:11-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/smt/assignment?rev=1255989491&do=diff SMT-LIB input format SMT-LIB home-page, SMT-LIB input format specification Salient features: * A formula is a list of attributes: :logic, :extrapreds, :extrafuns, :assumption, :formula, :difficulty, :status, etc. * Prefix format, e.g. (+ (- a b) c). * Zero or more assumptions, exactly one formula. * Let expressions: e.g. :assumption (let (?x (bvadd y bv11[4])) (= ?x z)) * Flet expressions: e.g. :assumption (flet ($f (or x y)) (and $f z)) * Use :extrafuns, :extrapreds to declare … text/html 2009-04-21T23:57:26-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/parallel_programming/splash2?rev=1240383446&do=diff <http://kbarr.net/splash2.html> <http://www.capsl.udel.edu/splash/index.html> barnes Barnes-Hut method to simulate the interaction of a system of bodies (N-body problem) The SPLASH-2 implementation allows for multiple particles to be stored in each leaf cell of the space partition. text/html 2009-04-18T11:36:38-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/software_testing/project/ronsse1999recplay?rev=1240079798&do=diff Sources of non-determinism (apart from inputs): * System calls like random(), gettimeofday() * Interrupts * Traps * Signals * Uninitialized variables * Dangling pointers * Data races RecPlay enables using standard sequential debugger to debug parallel programs. QUESTION: what does that mean? text/html 2009-04-15T11:39:34-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/verification/compositional/pasareanu2008learning?rev=1239820774&do=diff <http://www.citeulike.org/user/rhishi/article/3642638> This is a journal paper summarizing the framework for automated assumption generation using automaton learning algorithm L* for compositional model checking of safety properties. Applies to asymmetric as well as symmetric assume-guarantee rules. text/html 2009-04-14T23:43:13-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/pointer_analysis/start?rev=1239777793&do=diff Given a pointer expression in a program, what are the possible locations to which it may point. Locations are objects allocated by say malloc or new. context-insensitive pointer analysis with on-the-fly call graph construction Two steps: * Collecting program facts in the form of relations. * Writing datalog rules for pointer analysis using these relations. text/html 2009-04-08T18:55:58-07:00 rhishi http://www.ocf.berkeley.edu/~rhishi/wiki/software_testing/ocallahan2003hybrid?rev=1239242158&do=diff This is a dynamic race detector that combines two dynamic techniques -- lockset-based detection and happens-before detection. Advantages: * Fewer false positives than lockset-based. * Reports more information about potential races found. * Reduces overhead by not relying on happens-before relation alone, by discarding redundant information, and by using a two-phase approach to first identify error-prone program points. * Improves scalability by eliminating the need for whole-program s…