ORCID Profile
0000-0002-2352-1883
Current Organisation
University of Stuttgart
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
In Research Link Australia (RLA), "Research Topics" refer to ANZSRC FOR and SEO codes. These topics are either sourced from ANZSRC FOR and SEO codes listed in researchers' related grants or generated by a large language model (LLM) based on their publications.
Computer Software | Programming Languages | Computational Logic and Formal Languages | Programming Languages | Software Engineering | Computer System Security
Computer Software and Services not elsewhere classified | Computer software and services not elsewhere classified |
Publisher: Springer Berlin Heidelberg
Date: 2005
DOI: 10.1007/11609773_1
Publisher: Springer Berlin Heidelberg
Date: 2002
Publisher: Springer Berlin Heidelberg
Date: 2016
Publisher: Cambridge University Press (CUP)
Date: 23-09-2021
DOI: 10.1017/S1471068421000272
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.
Publisher: Springer Berlin Heidelberg
Date: 1997
DOI: 10.1007/BFB0032740
Publisher: Association for Computing Machinery (ACM)
Date: 03-1993
Abstract: We show how precise groundness information can be extracted from logic programs. The idea is to use abstract interpretation with Boolean functions as “approximations” to groundness dependencies between variables. This idea is not new, and different classes of Boolean functions have been used. We argue, however, that one class, the positive functions, is more suitable than others. Positive Boolean functions have a certain property which we (inspired by A. Langen) call “condensation.” This property allows for rapid computation of groundness information.
Publisher: World Scientific Pub Co Pte Lt
Date: 04-2007
DOI: 10.1142/S0129054107004668
Abstract: We present a new method for finding closed forms of recursive Boolean function definitions. Traditionally, these closed forms are found by Kleene iteration: iterative approximation until a fixed point is reached. Conceptually, our new method replaces each k-ary function by 2 k Boolean constants defined by mutual recursion. The introduction of an exponential number of constants is mitigated by the simplicity of their definitions and by the use of a novel variant of ROBDDs to avoid repeated computation. Experiments suggest that this approach is significantly faster than Kleene iteration for ex les that require many Kleene iteration steps.
Publisher: Association for Computing Machinery (ACM)
Date: 27-06-1999
Abstract: Computer animation is an excellent medium for capturing the dynamic nature of data structure manipulations, and can be used to advantage in the teaching of algorithms and data structures. A major educational issue is the necessity of providing a means for the student to manage the complexity of the material. We have addressed this issue in a multimedia teaching tool called "Algorithms in Action" by allowing students to view an algorithm at varying levels of detail. Starting with a high level pseudocode description of the algorithm, with accompanying high level animation and textual explanation, students can expand sections of the pseudocode to expose more detail. Animation and explanation are controlled in a coordinated fashion, becoming correspondingly more detailed as the pseudocode is expanded. The tool also supports dofferem , pdes. corresponding to different stages in the learning process. Student feedback suggests that the availability of multiple levels detail and the facility for the user to control the level of detail being viewed is an effective way to manage content complexity.
Publisher: IEEE
Date: 09-2015
Publisher: Springer International Publishing
Date: 2017
Publisher: Springer Berlin Heidelberg
Date: 2013
Publisher: Springer Science and Business Media LLC
Date: 02-1989
DOI: 10.1007/BF01806312
Publisher: Springer Berlin Heidelberg
Date: 1985
Publisher: Springer Berlin Heidelberg
Date: 1996
Publisher: ACM
Date: 14-05-2016
Publisher: Springer International Publishing
Date: 2021
Publisher: Springer International Publishing
Date: 2016
Publisher: Springer Science and Business Media LLC
Date: 05-1990
DOI: 10.1007/BF00277387
Publisher: IEEE
Date: 2016
Publisher: Cambridge University Press (CUP)
Date: 03-06-2013
DOI: 10.1017/S1471068413000069
Abstract: The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood but also for “undefined”. The three-valued semantics proposed by Fitting (Fitting, M. 1985. A Kripke–Kleene semantics for logic programs. Journal of Logic Programming 2 , 4, 295–312) and Kunen (Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4 , 4, 289–308) are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being associated with underspecification. Naish used an (apparently) novel “arrow” operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Belnap's four-valued logic (Belnap, N. D. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic , J. M. Dunn and G. Epstein, Eds. D. Reidel, Dordrecht, Netherlands, 8–37), also used elsewhere by Fitting, to unify the two three-valued approaches. The truth values are arranged in a bilattice, which supports the classical ordering on truth values as well as the “information ordering”. We note that the “arrow” operator of Naish (and our four-valued extension) is essentially the information ordering, whereas the classical arrow denotes the truth ordering. This allows us to shed new light on many aspects of logic programming, including program analysis, type and mode systems, declarative debugging and the relationships between specifications and programs, and successive execution states of a program.
Publisher: Springer Berlin Heidelberg
Date: 1995
Publisher: Association for Computing Machinery (ACM)
Date: 05-1989
DOI: 10.1145/66068.66075
Abstract: It is well-known that omission of the occur check in unification leads to unsound Prolog systems. Nevertheless, most Prolog systems omit the occur check because this makes unification much faster and unsoundness allegedly seldom manifests itself. We revisit the occur check problem and point to two aspects that have previously received no attention. Firstly, "unification without the occur check" is ambiguous, and in practice, Prolog systems vary markedly in their reaction to programs having occur check problems. Secondly, even very simple program transformations are unsafe for pure Prolog when the occur check is omitted. We conclude that the occur check problem is important, and in particular, that the current efforts to standardize Prolog should address it.
Publisher: Elsevier BV
Date: 04-1998
Publisher: ACM
Date: 16-06-2013
Publisher: Springer Berlin Heidelberg
Date: 1996
Publisher: Springer Science and Business Media LLC
Date: 06-1993
DOI: 10.1007/BF03037156
Publisher: Springer Berlin Heidelberg
Date: 1997
Publisher: Wiley
Date: 02-1998
DOI: 10.1002/(SICI)1097-024X(199802)28:2<199::AID-SPE150>3.0.CO;2-4
Publisher: Cambridge University Press (CUP)
Date: 07-2015
DOI: 10.1017/S1471068415000204
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.
Publisher: Springer Berlin Heidelberg
Date: 2010
Publisher: Springer Berlin Heidelberg
Date: 1998
DOI: 10.1007/BFB0056609
Publisher: Springer Berlin Heidelberg
Date: 2001
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 07-2014
Publisher: Elsevier BV
Date: 06-2010
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Open Publishing Association
Date: 26-07-2022
DOI: 10.4204/EPTCS.363.4
Publisher: Springer Science and Business Media LLC
Date: 08-11-2018
Publisher: Springer Berlin Heidelberg
Date: 1996
Publisher: Cambridge University Press (CUP)
Date: 07-2018
DOI: 10.1017/S1471068418000091
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.
Publisher: Association for Computing Machinery (ACM)
Date: 18-11-2014
DOI: 10.1145/2661632
Abstract: The use of nanoscale technologies to create electronic devices has revived interest in the use of regular structures for defining complex logic functions. One such structure is the switching lattice, a two-dimensional lattice of four-terminal switches. We show how to directly construct switching lattices of polynomial size from arbitrary logic functions we also show how to synthesize minimal-sized lattices by translating the problem to the satisfiability problem for a restricted class of quantified Boolean formulas. The synthesis method is an anytime algorithm that uses modern SAT solving technology and dichotomic search. It improves considerably on an earlier proposal for creating switching lattices for arbitrary logic functions.
Publisher: Springer Science and Business Media LLC
Date: 09-1995
DOI: 10.1007/BF01019002
Publisher: Springer Berlin Heidelberg
Date: 2016
Publisher: ACM
Date: 27-06-1999
Publisher: Association for Computing Machinery (ACM)
Date: 20-01-2015
DOI: 10.1145/2651360
Abstract: The most commonly used integer types have fixed bit-width, making it possible for computations to “wrap around,” and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.
Publisher: Springer Berlin Heidelberg
Date: 1988
Publisher: ACM
Date: 06-07-2009
Publisher: ACM
Date: 17-09-2002
Publisher: Association for Computing Machinery (ACM)
Date: 17-09-2002
Abstract: In this paper we present the first exception analysis for a non-strict language. We augment a simply-typed functional language with exceptions, and show that we can define a type-based inference system to detect uncaught exceptions. We have implemented this exception analysis in the GHC compiler for Haskell, which has been recently extended with exceptions. We give empirical evidence that the analysis is practical.
Publisher: ACM Press
Date: 1996
Publisher: Theory of Computing Exchange
Date: 2010
Publisher: ACM
Date: 16-06-2012
Publisher: Springer Berlin Heidelberg
Date: 2013
Publisher: Springer Science and Business Media LLC
Date: 07-2020
DOI: 10.1007/S00190-020-01395-3
Abstract: The 2004 Sumatra, 2010 Maule, and 2011 Tohoku great earthquakes triggered tsunamis as large as a few decimeters over a few 100 km in the open ocean. The transient ocean mass redistribution propagating as tsunamis changed the Earth’s gravity field enough to perturb the GRACE satellites’ orbits at ~ 500 km above the surface. The on-board microwave ranging system detected inter-satellite acceleration anomalies of up to 1.0–4.0 nm/s 2 . There is good agreement between GRACE measurements and tsunami models for the three events. Complementarily to buoys, ocean bottom pressure sounders, and satellite altimeters, GRACE is sensitive to the long-wavelength spatial scale of tsunamis and provides an independent source of information for assessing alternate early earthquake and tsunami models. Our study demonstrates an innovative way of applying GRACE and GRACE Follow-On data to detect transient geophysical mass changes which cannot be observed by the conventional monthly Level-2 and mascon solutions.
Publisher: IEEE
Date: 09-2015
Publisher: Association for Computing Machinery (ACM)
Date: 06-07-2009
Abstract: There are many different approaches to student peer assessment. In this paper I lay out the pedagogical philosophy behind my own use of student peer reviews. These should not only be seen as adding to the amount of formative feedback in a class, nor are they only about the development of certain higher-order cognitive skills. Properly aligned with an overall assessment strategy, peer reviewing can help build a stronger learning community. I describe such a strategy and my experience using PRAZE, an online tool for student peer reviewing, as well as students' response to the tool and its use.
Publisher: IEEE
Date: 10-2017
Publisher: Association for Computing Machinery (ACM)
Date: 08-1985
Publisher: Elsevier BV
Date: 04-2016
Publisher: Springer International Publishing
Date: 2015
Publisher: Informa UK Limited
Date: 12-2012
Publisher: Springer International Publishing
Date: 2015
Publisher: Association for Computing Machinery (ACM)
Date: 09-1999
Abstract: We investigate Jacobs and Langen's Sharing domain, introduced for the analysis of variable sharing in logic programs, and show that it is isomorphic to Marriott and Søndergaard's Pos domain, introduced for the analysis of groundness dependencies. Our key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to a recasting of sharing analysis in terms of the property of “not being affected by the binding of a single variable.” Such an “unaffectedness dependency” analysis has close connections with groundness dependency analysis using positive Boolean functions. This new view improves our understanding of sharing analysis, and leads to an elegant expression of its combination with groundness dependency analysis based on the reduced product of Sharing and Pos. It also opens up new avenues for the efficient implementation of sharing analysis, for ex le using reduced order binary decision diagrams, as well as efficient implementation of the reduced product, using domain factorizations.
Publisher: IEEE Comput. Soc
Date: 2000
Publisher: Association for the Advancement of Artificial Intelligence (AAAI)
Date: 10-05-2014
DOI: 10.1609/ICAPS.V24I1.13628
Abstract: We introduce a novel algorithm for temporal planning in Golog using shared resources, and describe the Bulk Freight Rail Scheduling Problem, a motivating ex le of such a temporal domain. We use the framework of column generation to tackle complex resource constrained temporal planning problems that are beyond the scope of current planning technology by combining: the global view of a linear programming relaxation of the problem the strength of search infinding action sequences and the domain knowledge that can be encoded in a Golog program. We show that our approach significantly outperforms state-of-the-art temporal planning and constraint programming approaches in this domain, in addition to existing temporal Golog implementations. We also apply our algorithm to a temporal variant of blocks-world where our decomposition speeds proof of optimality significantly compared to other anytime algorithms. We discuss the potential of the underlying algorithm being applicable to STRIPS planning, with further work.
Publisher: Springer Berlin Heidelberg
Date: 2009
Publisher: Springer Berlin Heidelberg
Date: 2008
Publisher: Springer International Publishing
Date: 2019
Publisher: Springer Berlin Heidelberg
Date: 2001
Publisher: Association for Computing Machinery (ACM)
Date: 05-1994
Abstract: Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism (or proof procedure, viewing execution as theorem proving). Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation . We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.
Publisher: Association for Computing Machinery (ACM)
Date: 02-1988
DOI: 10.1145/43908.43910
Publisher: Springer Berlin Heidelberg
Date: 2017
Publisher: Association for Computing Machinery (ACM)
Date: 03-09-2021
DOI: 10.1145/3457885
Abstract: Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.
Publisher: Springer Berlin Heidelberg
Date: 1999
Publisher: Springer International Publishing
Date: 2019
Publisher: IEEE
Date: 11-2018
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Date: 2020
Publisher: Springer Berlin Heidelberg
Date: 1986
Publisher: Springer Berlin Heidelberg
Date: 2007
Publisher: Elsevier BV
Date: 05-1998
Publisher: Springer Berlin Heidelberg
Date: 25-12-2016
Publisher: Elsevier BV
Date: 07-1992
Publisher: Informa UK Limited
Date: 09-2001
Publisher: Springer Berlin Heidelberg
Date: 1994
Publisher: Oxford University Press (OUP)
Date: 10-1992
Publisher: IEEE
Date: 06-2019
Publisher: IEEE
Date: 2004
Publisher: Springer Berlin Heidelberg
Date: 2013
Publisher: Springer Berlin Heidelberg
Date: 2016
Publisher: Springer International Publishing
Date: 2022
Publisher: Cambridge University Press (CUP)
Date: 07-2013
DOI: 10.1017/S1471068413000379
Abstract: We present a new execution strategy for constraint logic programs called Failure Tabled CLP . Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method only learns from failed derivations . This allows us to compute interpolants rather than constraint projection for generation of reuse conditions . As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.
Publisher: Springer International Publishing
Date: 2021
Publisher: Springer International Publishing
Date: 2021
Start Date: 2001
End Date: 2004
Funder: Australian Research Council
View Funded ActivityStart Date: 2003
End Date: 2006
Funder: Australian Research Council
View Funded ActivityStart Date: 1996
End Date: 1999
Funder: Australian Research Council
View Funded ActivityStart Date: 1995
End Date: 1998
Funder: Australian Research Council
View Funded ActivityStart Date: 1992
End Date: 1995
Funder: Australian Research Council
View Funded ActivityStart Date: 1991
End Date: 1993
Funder: Australian Research Council
View Funded ActivityStart Date: 2016
End Date: 2018
Funder: Australian Research Council
View Funded ActivityStart Date: 2011
End Date: 2013
Funder: Australian Research Council
View Funded ActivityStart Date: 2014
End Date: 2016
Funder: Australian Research Council
View Funded ActivityStart Date: 2003
End Date: 12-2007
Amount: $360,000.00
Funder: Australian Research Council
View Funded ActivityStart Date: 05-2015
End Date: 12-2019
Amount: $405,591.00
Funder: Australian Research Council
View Funded ActivityStart Date: 2011
End Date: 12-2015
Amount: $479,000.00
Funder: Australian Research Council
View Funded ActivityStart Date: 07-2014
End Date: 07-2018
Amount: $385,000.00
Funder: Australian Research Council
View Funded Activity