Search

Your search keyword '"Schachte, Peter"' showing total 147 results
Start Over Author "Schachte, Peter"
147 results on '"Schachte, Peter"'

2. Transformation-Enabled Precondition Inference

Author

Kafle, Bishoksan, Gange, Graeme, Stuckey, Peter J., Schachte, Peter, and Sondergaard, Harald

Subjects
Computer Science - Programming Languages
Abstract

Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states; which are used to partition the program's initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods., Comment: Paper presented at the 37th InternationalConference on Logic Programming (ICLP 2021), 16 pages. arXiv admin note: substantial text overlap with arXiv:1811.06771

Published
2021
Full Text
View/download PDF

3. Precondition Inference via Partitioning of Initial States

Author

Kafle, Bishoksan, Gange, Graeme, Schachte, Peter, Sondergaard, Harald, and Stuckey, Peter J.

Subjects
Computer Science - Logic in Computer Science
Abstract

Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of \emph{safe} and \emph{unsafe} \emph{initial} states. Then we repeatedly use the current abstractions to partition the program's \emph{initial} states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods., Comment: 19 pages, 8 figures

Published
2018

4. An iterative approach to precondition inference using constrained Horn clauses

Author

Kafle, Bishoksan, Gallagher, John P., Gange, Graeme, Schachte, Peter, Sondergaard, Harald, and Stuckey, Peter J.

Subjects
Computer Science - Logic in Computer Science
Abstract

We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions., Comment: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX

Published
2018

5. Lightweight Nontermination Inference with CHCs

Author

Kafle, Bishoksan, Gange, Graeme, Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Calinescu, Radu, editor, and Păsăreanu, Corina S., editor

Published
2021
Full Text
View/download PDF

6. Disjunctive Interval Analysis

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Drăgoi, Cezara, editor, Mukherjee, Suvam, editor, and Namjoshi, Kedar, editor

Published
2021
Full Text
View/download PDF

7. Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study

Author

Amadini, Roberto, Gange, Graeme, Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Fernández, Maribel, editor

Published
2021
Full Text
View/download PDF

8. Horn Clauses as an Intermediate Representation for Program Analysis and Transformation

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Sondergaard, Harald, and Stuckey, Peter J.

Subjects
Computer Science - Programming Languages
Abstract

Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation., Comment: To Appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015

Published
2015
Full Text
View/download PDF

9. A Complete Refinement Procedure for Regular Separability of Context-Free Languages

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Sondergaard, Harald, and Stuckey, Peter J.

Subjects
Computer Science - Formal Languages and Automata Theory
Abstract

Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present an effective semi-decision procedure for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two refinement methods, one inexpensive but incomplete, and the other complete but more expensive. We provide an experimental evaluation of this procedure, and demonstrate its practicality on a range of verification and language-theoretic instances.

Published
2014

10. Dissecting Widening: Separating Termination from Information

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Lin, Anthony Widjaja, editor

Published
2019
Full Text
View/download PDF

11. Constraint Programming for Dynamic Symbolic Execution of JavaScript

Author

Amadini, Roberto, Andrlon, Mak, Gange, Graeme, Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Rousseau, Louis-Martin, editor, and Stergiou, Kostas, editor

Published
2019
Full Text
View/download PDF

12. A Partial-Order Approach to Array Content Analysis

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Sondergaard, Harald, and Stuckey, Peter J.

Subjects
Computer Science - Programming Languages, D.2.4, D.3.1, F.3.1, F.3.2
Abstract

We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and Sagiv, and of Halbwachs and Peron. However, it introduces a novel concept of an array content graph, avoiding the need for an up-front factorial partitioning step. The resulting analysis can be used with arbitrary numeric relational abstract domains; we evaluate the domain on a range of array manipulating program fragments.

Published
2014

13. Disjunctive Interval Analysis

Author

Gange, Graeme, primary, Navas, Jorge A., additional, Schachte, Peter, additional, Søndergaard, Harald, additional, and Stuckey, Peter J., additional

Published
2021
Full Text
View/download PDF

16. Estimating the overlap between dependent computations for automatic parallelization

Author

Bone, Paul, Somogyi, Zoltan, and Schachte, Peter

Subjects
Computer Science - Programming Languages, Computer Science - Distributed, Parallel, and Cluster Computing
Abstract

Researchers working on the automatic parallelization of programs have long known that too much parallelism can be even worse for performance than too little, because spawning a task to be run on another CPU incurs overheads. Autoparallelizing compilers have therefore long tried to use granularity analysis to ensure that they only spawn off computations whose cost will probably exceed the spawn-off cost by a comfortable margin. However, this is not enough to yield good results, because data dependencies may \emph{also} limit the usefulness of running computations in parallel. If one computation blocks almost immediately and can resume only after another has completed its work, then the cost of parallelization again exceeds the benefit. We present a set of algorithms for recognizing places in a program where it is worthwhile to execute two or more computations in parallel that pay attention to the second of these issues as well as the first. Our system uses profiling information to compute the times at which a procedure call consumes the values of its input arguments and the times at which it produces the values of its output arguments. Given two calls that may be executed in parallel, our system uses the times of production and consumption of the variables they share to determine how much their executions would overlap if they were run in parallel, and therefore whether executing them in parallel is a good idea or not. We have implemented this technique for Mercury in the form of a tool that uses profiling data to generate recommendations about what to parallelize, for the Mercury compiler to apply on the next compilation of the program. We present preliminary results that show that this technique can yield useful parallelization speedups, while requiring nothing more from the programmer than representative input data for the profiling run.

Published
2011

17. Binary Decision Diagrams for Affine Approximation

Author

Henshall, Kevin, Schachte, Peter, Søndergaard, Harald, and Whiting, Leigh

Subjects
Computer Science - Logic in Computer Science, Computer Science - Artificial Intelligence
Abstract

Selman and Kautz's work on ``knowledge compilation'' established how approximation (strengthening and/or weakening) of a propositional knowledge-base can be used to speed up query processing, at the expense of completeness. In this classical approach, querying uses Horn over- and under-approximations of a given knowledge-base, which is represented as a propositional formula in conjunctive normal form (CNF). Along with the class of Horn functions, one could imagine other Boolean function classes that might serve the same purpose, owing to attractive deduction-computational properties similar to those of the Horn functions. Indeed, Zanuttini has suggested that the class of affine Boolean functions could be useful in knowledge compilation and has presented an affine approximation algorithm. Since CNF is awkward for presenting affine functions, Zanuttini considers both a sets-of-models representation and the use of modulo 2 congruence equations. In this paper, we propose an algorithm based on reduced ordered binary decision diagrams (ROBDDs). This leads to a representation which is more compact than the sets of models and, once we have established some useful properties of affine Boolean functions, a more efficient algorithm., Comment: 15 pages

Published
2008

18. Combining String Abstract Domains for JavaScript Analysis: An Evaluation

Author

Amadini, Roberto, Jordan, Alexander, Gange, Graeme, Gauthier, François, Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Zhang, Chenyi, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Legay, Axel, editor, and Margaria, Tiziana, editor

Published
2017
Full Text
View/download PDF

19. A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic

Author

Kafle, Bishoksan, Gange, Graeme, Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Gaspers, Serge, editor, and Walsh, Toby, editor

Published
2017
Full Text
View/download PDF

20. Minimizing Landscape Resistance for Habitat Conservation

Author

de Uña, Diego, Gange, Graeme, Schachte, Peter, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Salvagnin, Domenico, editor, and Lombardi, Michele, editor

Published
2017
Full Text
View/download PDF

22. Exploiting Sparsity in Difference-Bound Matrices

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Rival, Xavier, editor

Published
2016
Full Text
View/download PDF

23. An Abstract Domain of Uninterpreted Functions

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Jobstmann, Barbara, editor, and Leino, K. Rustan M., editor

Published
2016
Full Text
View/download PDF

24. A Bounded Path Propagator on Directed Graphs

Author

de Uña, Diego, Gange, Graeme, Schachte, Peter, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Rueher, Michel, editor

Published
2016
Full Text
View/download PDF

25. Weighted Spanning Tree Constraint with Explanations

Author

de Uña, Diego, Gange, Graeme, Schachte, Peter, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Quimper, Claude-Guy, editor

Published
2016
Full Text
View/download PDF

28. Analyzing Array Manipulating Programs by Program Transformation

Author

Cornish, J. Robert M., Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Proietti, Maurizio, editor, and Seki, Hirohisa, editor

Published
2015
Full Text
View/download PDF

29. A Tool for Intersecting Context-Free Grammars and Its Applications

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Havelund, Klaus, editor, Holzmann, Gerard, editor, and Joshi, Rajeev, editor

Published
2015
Full Text
View/download PDF

31. Abstract Interpretation over Non-lattice Abstract Domains

Author

Gange, Graeme, Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Logozzo, Francesco, editor, and Fähndrich, Manuel, editor

Published
2013
Full Text
View/download PDF

32. Solving Difference Constraints over Modular Arithmetic

Author

Gange, Graeme, Søndergaard, Harald, Stuckey, Peter J., Schachte, Peter, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, and Bonacina, Maria Paola, editor

Published
2013
Full Text
View/download PDF

33. Unbounded Model-Checking with Interpolation for Regular Language Constraints

Author

Gange, Graeme, Navas, Jorge A., Stuckey, Peter J., Søndergaard, Harald, Schachte, Peter, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Piterman, Nir, editor, and Smolka, Scott A., editor

Published
2013
Full Text
View/download PDF

35. Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code

Author

Navas, Jorge A., Schachte, Peter, Søndergaard, Harald, Stuckey, Peter J., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Jhala, Ranjit, editor, and Igarashi, Atsushi, editor

Published
2012
Full Text
View/download PDF

36. State Joining and Splitting for the Symbolic Execution of Binaries

Author

Hansen, Trevor, Schachte, Peter, Søndergaard, Harald, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Bensalem, Saddek, editor, and Peled, Doron A., editor

Published
2009
Full Text
View/download PDF

41. Size-Change Termination Analysis in k-Bits

Author

Codish, Michael, Lagoon, Vitaly, Schachte, Peter, Stuckey, Peter J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Sestoft, Peter, editor

Published
2006
Full Text
View/download PDF

42. Closure Operators for ROBDDs

Author

Schachte, Peter, Søndergaard, Harald, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Emerson, E. Allen, editor, and Namjoshi, Kedar S., editor

Published
2006
Full Text
View/download PDF

43. Sequence Quantification

Author

Schachte, Peter, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Dahl, Veronica, editor, and Wadler, Philip, editor

Published
2003
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results