ScholarBank@NUShttps://scholarbank.nus.edu.sgThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Fri, 30 Sep 2022 00:53:56 GMT2022-09-30T00:53:56Z50111- A proof slicing framework for program verificationhttps://scholarbank.nus.edu.sg/handle/10635/77977Title: A proof slicing framework for program verification
Authors: Le, T.C.; Gherghina, C.; Voicu, R.; Chin, W.-N.
Abstract: In the context of program verification, we propose a formal framework for proof slicing that can aggressively reduce the size of proof obligations as a means of performance improvement. In particular, each large proof obligation may be broken down into smaller proofs, for which the overall processing cost can be greatly reduced, and be even more effective under proof caching. Our proposal is built on top of existing automatic provers, including the state-of-the-art prover Z3, and can also be viewed as a re-engineering effort in proof decomposition that attempts to avoid large-sized proofs for which these provers may be particularly inefficient. In our approach, we first develop a calculus that formalizes a complete proof slicing procedure, which is followed by the development of an aggressive proof slicing method. Retaining completeness is important, and thus in our experiments the complete method serves as a backup for the cases when the aggressive procedure fails. The foundations of the aggressive slicing procedure are based on a novel lightweight annotation scheme that captures weak links between sub-formulas of a proof obligation; the annotations can be inferred automatically in practice, and thus both methods are fully automated. © 2013 Springer-Verlag.
Tue, 01 Jan 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/779772013-01-01T00:00:00Z
- Modeling systems in CLPhttps://scholarbank.nus.edu.sg/handle/10635/40660Title: Modeling systems in CLP
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/406602005-01-01T00:00:00Z
- A CLP proof method for timed automatahttps://scholarbank.nus.edu.sg/handle/10635/41107Title: A CLP proof method for timed automata
Authors: Jaffar, J.; Santosa, A.; Voicu, R.
Abstract: Constraint Logic Programming (CLP) has been used to model programs and transition systems for the purpose of verification problems. In particular, it has been used to model Timed Safety Automata (TSA). In this paper, we start with a systematic translation of TSA into CLP. The main contribution is an expressive assertion language and a new CLP inference method for proving assertions. A distinction of the assertion language is that it can specify important properties beyond traditional safety properties. We highlight one important property: that a system of processes is symmetric. The new inference mechanism is based upon the well-known method of tabling in logic programming. It is distinguished by its ability to use assertions that are not yet proven, using a principle of coinduction. Apart from given assertions, the proof mechanism can also prove implicit assertions such as discovering a lower or upper bound of a variable. Finally, we demonstrate significant improvements over state-of-the-art systems using standard TSA benchmark examples. © 2004 IEEE.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411072004-01-01T00:00:00Z
- A coinduction rule for entailment of recursively defined propertieshttps://scholarbank.nus.edu.sg/handle/10635/41110Title: A coinduction rule for entailment of recursively defined properties
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: Recursively defined properties are ubiquitous. We present a proof method for establishing entailment of such properties and over a set of common variables. The main contribution is a particular proof rule based intuitively upon the concept of coinduction. This rule allows the inductive step of assuming that an entailment holds during the proof the entailment. In general, the proof method is based on an unfolding (and no folding) algorithm that reduces recursive definitions to a point where only constraint solving is necessary. The constraint-based proof obligation is then discharged with available solvers. The algorithm executes the proof by a search-based method which automatically discovers the opportunity of applying induction instead of the user having to specify some induction schema, and which does not require any base case. © 2008 Springer-Verlag Berlin Heidelberg.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411102008-01-01T00:00:00Z
- Efficient memoization for dynamic programming with ad-hoc constraintshttps://scholarbank.nus.edu.sg/handle/10635/41111Title: Efficient memoization for dynamic programming with ad-hoc constraints
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We address the problem of effective reuse of subproblem solutions in dynamic programming. In dynamic programming, a memoed solution of a subproblem can be reused for another if the latter's context is a special case of the former. Our objective is to generalize the context of the memoed subproblem such that more subproblems can be considered subcases and hence enhance reuse. Toward this goal we propose a generalization of context that 1) does not add better solutions than the subproblem's optimal, yet 2) requires that subsumed sub-problems preserve the optimal solution. In addition, we also present a general technique to search for at most k ≥ 1 optimal solutions. We provide experimental results on resource-constrained shortest path (RCSP) benchmarks and program's exact worst-case execution time (WCET) analysis. Copyright © 2008, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411112008-01-01T00:00:00Z
- An interpolation method for CLP traversalhttps://scholarbank.nus.edu.sg/handle/10635/41103Title: An interpolation method for CLP traversal
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We consider the problem of exploring the search tree of a CLP goal in pursuit of a target property. Essential to such a process is a method of tabling to prevent duplicate exploration. Typically, only actually traversed goals are memoed in the table. In this paper we present a method where, upon the successful traversal of a subgoal, a generalization of the subgoal is memoed. This enlarges the record of already traversed goals, thus providing more pruning in the subsequent search process. The key feature is that the abstraction computed is guaranteed not to give rise to a spurious path that might violate the target property. A driving application area is the use of CLP to model the behavior of other programs. We demonstrate the performance of our method on a benchmark of program verfication problems. © 2009 Springer Berlin Heidelberg.
Thu, 01 Jan 2009 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411032009-01-01T00:00:00Z
- A specialization calculus for pruning disjunctive predicates to support verificationhttps://scholarbank.nus.edu.sg/handle/10635/42073Title: A specialization calculus for pruning disjunctive predicates to support verification
Authors: Chin, W.-N.; Gherghina, C.; Voicu, R.; Le, Q.L.; Craciun, F.; Qin, S.
Abstract: Separation logic-based abstraction mechanisms, enhanced with user-defined inductive predicates, represent a powerful, expressive means of specifying heap-based data structures with strong invariant properties. However, expressive power comes at a cost: the manipulation of such logics typically requires the unfolding of disjunctive predicates which may lead to expensive proof search. We address this problem by proposing a predicate specialization technique that allows efficient symbolic pruning of infeasible disjuncts inside each predicate instance. Our technique is presented as a calculus whose derivations preserve the satisfiability of formulas, while reducing the subsequent cost of their manipulation. Initial experimental results have confirmed significant speed gains from the deployment of predicate specialization. While specialization is a familiar technique for code optimization, its use in program verification is new. © 2011 Springer-Verlag.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/420732011-01-01T00:00:00Z
- A CLP method for compositional and intermittent predicate abstractionhttps://scholarbank.nus.edu.sg/handle/10635/40121Title: A CLP method for compositional and intermittent predicate abstraction
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We present an implementation of symbolic reachability analysis with the features of compositionality, and intermittent abstraction, in the sense of pefrorming approximation only at selected program points, if at all. The key advantages of compositionality are well known, while those of intermittent abstraction are that the abstract domain required to ensure convergence of the algorithm can be minimized, and that the cost of performing abstractions, now being intermittent, is reduced. We start by formulating the problem in CLP, and first obtain compositionality. We then address two key efficiency challenges. The first is that reasoning is required about the strongest-postcondition operator associated with an arbitrarily long program fragment. This essentially means dealing with constraints over an unbounded number of variables describing the states between the start and end of the program fragment at hand. This is addressed by using the variable elimination or projection mechanism that is implicit in CLP systems. The second challenge is termination, that is, to determine which subgoals are redundant. We address this by a novel formulation of memoization called coinductive tabling. We finally evaluate the method experimentally. At one extreme, where abstraction is performed at every step, we compare against a model checker. At the other extreme, where no abstraction is performed, we compare against a program verifier. Of course, our method provides for the middle ground, with a flexible combination of abstraction and Hoare-style reasoning with predicate transformers and loop-invariants. © Springer-Verlag Berlin Heidelberg 2006.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/401212006-01-01T00:00:00Z
- Relative safetyhttps://scholarbank.nus.edu.sg/handle/10635/40122Title: Relative safety
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: A safety property restricts the set of reachable states. In this paper, we introduce a notion of relative safety which states that certain program states are reachable provided certain other states are. A key, but not exclusive, application of this method is in representing symmetry in a program. Here, we show that relative safety generalizes the programs that are presently accommodated by existing methods for symmetry. Finally, we provide a practical algorithm for proving relative safety. © Springer-Verlag Berlin Heidelberg 2006.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/401222006-01-01T00:00:00Z
- Framework for combining analysis and verificationhttps://scholarbank.nus.edu.sg/handle/10635/40247Title: Framework for combining analysis and verification
Authors: Heintze, N.; Jaffar, J.; Voicu, R.
Abstract: We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features: it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.
Sat, 01 Jan 2000 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/402472000-01-01T00:00:00Z
- Language-Based Program Verification via Expressive Typeshttps://scholarbank.nus.edu.sg/handle/10635/39801Title: Language-Based Program Verification via Expressive Types
Authors: Sulzmann, M.; Voicu, R.
Abstract: Recent developments in the area of expressive types have the prospect to supply the ordinary programmer with a programming language rich enough to verify complex program properties. Program verification is made possible via tractable type checking. We explore this possibility by considering two specific examples; verifying sortedness and resource usage verification. We show that advanced type error diagnosis methods become essential to assist the user in case of type checking failure. Our results point out new research directions for the development of programming environments in which users can write and verify their programs. © 2007 Elsevier B.V. All rights reserved.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/398012007-01-01T00:00:00Z