:- expects_dialect(sicstus).
% this is the prolog database of papers (almost like bibtex).
% in a better world this would be produced using a parser from 
% a bibtex file.


:- module(papers, [bibentry/3]).


%%% JOURNAL PAPERS
/*
bibentry(article,'',
[ author   = '',       
  title    = '',       
  journal  = '',     
  year     = '',         
  volume   = '',       
  number   = '',       
  pages    = '',        
  abstract = '',      
                 
  available = [],    
  related   = []     
                 
  ] ).
*/

% jcss

bibentry(article,'jcssB',
[ author = ['Daniel Bundala',codish,'Luis Cruz-Filipe',psk,'Jakub Zavodny'],
  title  = 'Optimal-Depth Sorting Networks',
  abstract = '
     We solve a 40-year-old open problem on the depth optimality of
     sorting networks.  In 1973, Donald E.~Knuth detailed, in Volume~3 of
     The Art of Computer Programming, sorting networks of the smallest
     depth known at the time for n =< 16 inputs, quoting optimality for n
     =< 8.  In 1989, Parberry proved the optimality of the networks with 9
     =< n =< 10 inputs.  In this article, we present a general technique
     for obtaining such optimality results, and use it to prove the
     optimality of the remaining open cases of 11 =< n =< 16 inputs.  We
     show how to exploit symmetry to construct a small set of two-layer
     networks on $n$ inputs such that if there is a sorting network on $n$
     inputs of a given depth, then there is one whose first layers are in
     this set.  For each network in the resulting set, we construct a
     propositional formula whose satisfiability is necessary for the
     existence of a sorting network of a given depth. Using an
     off-the-shelf SAT solver we show that the sorting networks listed by
     Knuth are optimal. For n =< 10 inputs, our algorithm is orders of
     magnitude faster than the prior ones.',
  journal  = 'Journal of Computer and System Sciences',     
  year     = 2016,         
  volume   = ' (accepted)',       
  number   = '?',       
  pages    = '?',
  related =  [],
  available = []
]).


bibentry(article,'jcssA',
[ author = [codish,'Luis Cruz-Filipe','Michael Frank',psk],
  title  = 'Sorting nine inputs requires twenty-five comparisons',
  abstract = '
    Twenty-five comparators are minimal to sort nine inputs.Twenty-nine
    comparators are minimal to sort ten inputs.New symmetry-breaking
    results control the growth of the search space.Optimized and
    parallelized algorithms for generating size-optimal sorting
    networks.Use of SAT-solving to speed up the last part of the
    computation. This paper describes a computer-assisted non-existence
    proof of 9-input sorting networks consisting of 24 comparators, hence
    showing that the 25-comparator sorting network found by Floyd in 1964
    is optimal. As a corollary, the 29-comparator network found by Waksman
    in 1969 is optimal when sorting 10 inputs.This closes the two smallest
    open instances of the optimal-size sorting network problem, which have
    been open since the results of Floyd and Knuth from 1966 proving
    optimality for sorting networks of up to 8 inputs.
',
  journal  = 'Journal of Computer and System Sciences',     
  year     = 2016,         
  volume   = '82',       
  number   = '3',       
  pages    = '551-563',
  related =  [(url('http://arxiv.org/abs/1405.5754'),
            'e-print from arXiv.org'),
              (url('http://dl.acm.org/citation.cfm?id=2874752'),'ACM Digital Library')],
  available = []
]).


bibentry(article,'constraints16b',
[ author   = ['Avraham Itzhakov', codish],     
  title    = 'Breaking Symmetries in Graph Search with Canonizing Sets',       
  journal  = 'Constraints',     
  year     = 2016,         
  volume   = '21',       
  number   = '3',       
  pages    = '357--374',
  abstract = '
  There are many complex combinatorial problems which involve
  searching for an undirected graph satisfying given constraints. 
  Such problems are often highly challenging because of the
  large number of isomorphic representations of their solutions.
  This paper introduces effective and compact, complete symmetry
  breaking constraints for small graph search.
  Enumerating with these symmetry breaks generates all and
  only non-isomorphic solutions.
  For small search problems, with up to $10$ vertices, we compute
  instance independent symmetry breaking constraints.
  For small search problems with a larger number of vertices we
  demonstrate the computation of instance dependent constraints which
  are complete.
  We illustrate the application of complete symmetry breaking
  constraints to extend two known sequences from the OEIS
  related to graph enumeration.
  We also demonstrate the application of a generalization of our
  approach to fully-interchangeable matrix search problems.
  ',        
  available = [],    
  related   = [(url('http://arxiv.org/abs/1511.08205'),'from the arXiv'),
               (url('http://link.springer.com/article/10.1007/s10601-016-9244-z'),'from springer'),
               (url('https://www.cs.bgu.ac.il/~mcodish/Papers/Tools/canonizingSets/'),'canonizing sets for small graphs')
]                 
  ] ).



bibentry(article,'constraints16a',
[ author   = [codish, 'Michael Frank', 'Avraham Itzhakov', 'Alice Miller'],     
  title    = 'Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking',       
  journal  = 'Constraints',     
  year     = 2016,         
  volume   = '21',       
  number   = '3',       
  pages    = '375--393',
  abstract = '
The number R(4, 3, 3) is often presented as the unknown Ramsey number
with the best chances of being found “soon”. Yet, its precise value
has remained unknown for almost 50 years. This paper presents a
methodology based on abstraction and symmetry breaking that applies to
solve hard graph edge-coloring problems. The utility of this
methodology is demonstrated by using it to compute the value R(4, 3,
3) = 30. Along the way it is required to first compute the previously
unknown set of (3,3,3;13) colorings consisting of 78,892 Ramsey colorings.  ',        
  available = [],    
  related   = [(url('http://arxiv.org/abs/1510.08266'),'from the arXiv'),
               (url('http://link.springer.com/article/10.1007/s10601-016-9240-3'),
            'from Springer')]                 
  ] ).

bibentry(article,'jair13',
[ author   = ['Amit Metodi', codish,  pjs],     
  title    = 'Boolean Equi-propagation for Concise and Efficient SAT Encodings of
              Combinatorial Problems',       
  journal  = 'Journal of Artificial Intelligence Research',     
  year     = 2013,         
  volume   = '46',       
  number   = ' ',       
  pages    = '303-341',
  abstract = 'We present an approach to propagation-based SAT encoding of
  combinatorial problems, Boolean equi-propagation, where constraints
  are modeled as Boolean functions which propagate information about
  equalities between Boolean literals.  This information is then
  applied to simplify the CNF encoding of the constraints.
  A key factor is that considering only a small fragment of a
  constraint model at one time enables us to apply stronger, and even
  complete, reasoning to detect equivalent literals in that
  fragment. Once detected, equivalences apply to simplify the entire
  constraint model and facilitate further reasoning on other
  fragments.
  Equi-propagation in combination with partial evaluation and
  constraint simplification provide the foundation for a powerful
  approach to SAT-based finite domain constraint solving. 
  We introduce a tool called BEE (Ben-Gurion Equi-propagation
  Encoder) based on these ideas and
  demonstrate for a variety of benchmarks that our approach leads
  to a considerable reduction in the size of CNF encodings and
  subsequent speed-ups in SAT solving times.',      
                 
  available = ['pdf'],    
  related   = []     
                 
  ] ).


bibentry(article,'pairwiseSelection',
[ author   = ['Moshe Zazon-Ivry', codish],     
  title    = 'Pairwise Networks are Superior for Selection',       
  journal  = '(submitted)',     
  year     = 2012,         
  volume   = '?',       
  number   = '?',       
  pages    = '?',        
  abstract = 
   'This paper revisits the pairwise sorting network introduced by
  Parberry in the early 90s. We provide a simple specification of the
  pairwise network which also clarifies its close resemblance to the
  more classic odd-even network introduced by Batcher in the mid 60s.
  Finally we illustrate that pairwise networks are better suited than
  odd-even networks for the construction of selection networks.', 
   available = ['pdf'], 
   related = [] ] ).


bibentry(article,'bee',
[ author   = ['Amit Metodi', codish],     
  title    = 'Compiling Finite Domain
              Constraints to SAT with BEE',       
  journal  = 'Theory and Practice of Logic Programming',     
  year     = 2012,         
  volume   = 12,       
  number   = '4-5',       
  pages    = '465--483',        
  abstract = 
   'We present BEE, a compiler which enables to encode finite domain
  constraint problems to CNF. Using BEE both eases the encoding
  process for the user and also performs transformations to simplify
  constraints and optimize their encoding to CNF. These optimizations
  are based primarily on equi-propagation and on partial evaluation,
  and also on the idea that a given constraint may have various
  possible CNF encodings. Often, the better encoding choice is made
  after constraint simplification. BEE is written in Prolog and
  integrates directly with a SAT solver through a suitable Prolog
  interface. We demonstrate that constraint simplification is often
  highly beneficial when solving hard finite domain constraint
  problems. A  BEE implementation is available with this
  paper. ', 
   available = [], 
   related = [
           (url('http://arxiv.org/abs/1206.3883'),
            'available on arxiv'),
           (url('http://amit.metodi.me/research/bee/'),
            'an implementation')] 
] ).





bibentry(article,'mcnp',
[ author   = [codish,'Igor Gonopolskiy','Amir Ben-Amram',
                            'Carsten Fuhs','J&uuml;rgen Giesl'],     
  title    = 'SAT-Based Termination Analysis Using 
    Monotonicity Constraints over the Integers',       
  journal  = 'Theory and Practice of Logic Programming',     
  year     = 2011,         
  volume   = '11',       
  number   = '4-5',       
  pages    = '503--520',        
  abstract = 
   'We describe an algorithm for proving termination of programs
    abstracted to systems of monotonicity constraints in the integer
  domain.  Monotonicity constraints are a non-trivial extension of the
  well-known size-change termination method.  While deciding
  termination for systems of monotonicity constraints is PSPACE
  complete, we focus on a well-defined and significant subset, which
  we call MCNP, designed to be amenable to a SAT-based solution.  Our
  technique is based on the search for a 
  special type of ranking function  
  defined in terms of bounded differences between multisets of integer
  values.  We describe the application of our approach as the back-end
  for the termination analysis of Java Bytecode (JBC). At the
  front-end, systems of monotonicity constraints are obtained by
  abstracting information, using two different termination analyzers:
  AProVE and Costa.  Preliminary results reveal that our approach
  provides a good trade-off between precision and cost of analysis.', 
   available = [], 
   related = [(url('http://arxiv.org/abs/1107.5980'),
            'available on arxiv')] ] ).

bibentry(article,'jar2011',
[ author   = [codish, 'J&uuml;rgen Giesl', psk,'Ren&eacute; Thiemann'],     
  title    = 'SAT Solving for Termination Proofs with 
              Recursive Path Orders and Dependency Pairs',       
  journal  = 'Journal of Automated Reasoning ',     
  year     = 2011,         
  volume   = 49,       
  number   = 1,       
  pages    = '53--93',        
  abstract = 
   'This paper introduces a propositional encoding for recursive path
   orders (RPO), in connection with dependency pairs. Hence, we
   capture in a uniform setting all common instances of RPO, i.e.,
   lexicographic path orders (LPO), multiset path orders (MPO), and
   lexicographic path orders with status (LPOS). This facilitates the
   application of SAT solvers for termination analysis of term rewrite
   systems (TRSs). We address four main inter-related issues and show
   how to encode them as satisfiability problems of propositional
   formulas that can be efficiently handled by SAT solving: (A) the
   lexicographic comparison w.r.t. a permutation of the arguments; (B)
   the multiset extension of a base order; (C) the combined search for
   a path order together with an argument filter to orient a set of
   inequalities; and (D) how the choice of the argument filter
   influences the set of inequalities that have to be oriented
   (so-called usable rules). We have implemented our contributions in
   the termination prover AProVE. Extensive experiments show that by
   our encoding and the application of SAT solvers one obtains
   speedups in orders of magnitude as well as increased termination
   proving power.', 
   available = [], 
   related = [] ] ).

bibentry(article,'constraints09',
[ author    = ['Olga Ohrimenko',pjs,codish],
  title     = 'Propagation via lazy clause generation',

  abstract = 'Finite domain propagation solvers effectively represent
  the possible values of variables by a set of choices which can be
  naturally modelled as Boolean variables. In this paper we describe
  how to mimic a finite domain propagation engine, by mapping
  propagators into clauses in a SAT solver. This immediately results
  in strong nogoods for finite domain propagation. But a naive static
  translation is impractical except in limited cases. We show how to
  convert propagators to lazy clause generators for a SAT solver. The
  resulting system introduces flexibility in modelling since variables
  are modelled dually in the propagation engine and the SAT solver,
  and we explore various approaches to the dual modelling. We show
  that the resulting system solves many finite domain problems
  significantly faster than other techniques.',
  journal = 'Constraints',
  volume    = '14',
  number = '3',
  publisher = 'Springer Netherlands',
  pages     = '357-391',
  year      = 2009,
  available = []  
]).




bibentry(article,'jsat2008',
[ author    = [codish,lagoon,pjs],
  title     = 'Solving Partial Order Constraints for LPO Termination',

  abstract = '    This paper introduces a propositional encoding for lexicographic
    path orders (LPOs) and the corresponding LPO termination property
    of term rewrite systems. Given this encoding, termination analysis
    can be performed using a state-of-the-art Boolean satisfiability
    solver.  Experimental results are unequivocal, indicating orders
    of magnitude speedups in comparison with previous implementations
    for LPO termination.
    The results of this paper have already had a direct impact on the
    design of several major termination analyzers for term rewrite
    systems.
    The contribution builds on a symbol-based approach towards
    reasoning about partial orders. The symbols in an unspecified
    partial order are viewed as variables that take integer values
    and are interpreted as indices in the order.
    For a partial order statement on $n$ symbols, each index is
    represented in log_2 n propositional variables and
    partial order constraints between symbols are modeled on the bit
    representations.
    The proposed encoding is general and relevant to other applications
    which involve propositional reasoning about partial orders.',
  journal = 'Journal on Satisfiability, Boolean Modeling and Computation (JSAT)',
  volume    = '5',
  publisher = 'Delft University in cooperation with IOS Press',
  pages     = '193-215',
  year      = 2008,
  month     = 'June',
  related =      [
           (url('
             http://jsat.ewi.tudelft.nl/content/volume5/JSAT5_7_Codish.pdf'),
            'JSAT online version')],
  available = ['pdf']  
]).





bibentry(article,'lpsat',
[ author = [codish,lagoon,pjs],
  title  = 'Logic Programming with Satisfiability',
  abstract = 'This paper presents a Prolog interface to the MiniSat
  satisfiability solver. Logic programming with satisfiability
  combines the strengths of the two paradigms: logic programming for
  encoding search problems into satisfiability on the one hand and
  efficient SAT solving on the other. This synergy between these two
  exposes a programming paradigm which we propose here as a logic
  programming pearl.  To illustrate logic programming with SAT solving
  we detail a Prolog program which solves instances of Partial MAXSAT
  and motivate the relation of this problem to termination analysis.',
  institution = 'Department of Computer Science; 
                 Ben-Gurion University',
  year      = 2008,     
  journal  = 'Theory and Practice of Logic Programming',    
  volume   = '8',
  number   = '1',
  pages    = '121-128',
  month     = 'January',
  related =      [(off_home('Software/pl-minisat.tgz'), 'SWI Interface to MiniSat')],
  available = ['pdf']
]).



bibentry(article,'comb_types',
    [ author = [maurice,codish,john,genaim,wim],
      title = 'Termination Analysis through Combination of Type Based Norms',
      abstract =
       '  This paper makes two contributions to the work on semantics based termination
  analysis for logic programs.
  The first involves a novel notion of typebased norm where for a
  given type a corresponding norm is defined to count in a term the number of
  sub-terms of that type. This provides a collection of candidate norms, one
  for each type defined in the program.
  The second enables an analyser to base termination proofs on the
  combination of several different norms.  This is useful when different norms
  are better suited to justify the termination of different parts of the
  program.
  Application of the two contributions together consists in considering the
  combination of the typebased candidate norms for a given program. This
  results in a powerful and practical technique.
  Both contributions have been introduced into a working termination
  analyser.  
  Experimentation indicates that they yield state-of-the-art results
  in a fully automatic analysis tool,  improving with respect to 
  methods that do not use both types and combined norms.',

  year      = 2007,
  journal =  'ACM Transactions on Programming Languages and Systems',
  volume   = '29',
  number   = '2',
  pages    = '10',
  related =      [ (paper('vmcai02'), 'Preliminary paper on combining norms'),
           (url('
http://doi.acm.org/10.1145/1216374.1216378'),
            'from the ACM Portal')],
  available = ['ps']
]).






bibentry(article,'backwards',
[ author   = [genaim,codish],       
  title    = 'Inferring Termination Conditions for Logic  
        Programs using Backwards Analysis',       
  journal  = 'Theory and Practice of Logic Programming',     
  year     = 2004,         
  volume   = '',       
  number   = 'accepted',       
  pages    = '',        
  abstract = ' This paper focuses on the inference of modes for which
  a logic program is guaranteed to terminate. This generalises
  traditional termination analysis where an analyser tries to verify
  termination for a specified mode.  Our contribution is a methodology
  in which components of traditional termination analysis are combined
  with backwards analysis to obtain an analyser for termination
  inference.  We identify a condition on the components of the
  analyser which guarantees that termination inference will infer all
  modes which can be checked to terminate.  The application of this
  methodology to enhance a traditional termination analyser to perform
  also termination inference is demonstrated.',
  available = [ps],    
  related   = [(source('lpar01.ps'), 'conference version')]            
  ] ).



bibentry(inproceedings,'meta_circ',
[ author = [codish,harald],
  title  = 'Meta-circular abstract interpretation in Prolog',
  booktitle =  'The Essence of Computation: Complexity, Analysis,
                Transformation',
  abstract = 'We give an introduction to the meta-circular approach to
     the abstract interpretation of logic programs.  This approach is
     particularly useful for prototyping and for introductory classes
     on abstract interpretation.  Using interpreters, students can
     immediately write, adapt, and experiment with interpreters and
     working dataflow analysers.  We use a simple meta-circular
     interpreter, based on a "non-ground Tp" semantics, as a
     generic analysis engine.  Instantiating the engine is a matter of
     providing an appropriate domain of approximations, together with
     definitions of "abstract" unification and disjunction.  Small
     changes of the interpreter let us vary both what can be
     "observed" by an analyser, and how fixed point computation is
     done.  Amongst the dataflow analyses used to exemplify this
     approach are a parity analysis, groundness dependency analysis,
     call patterns, depth-k analysis, and a "pattern" analysis to
    establish most specific generalisations of calls and success
     sets.',
  year      = 2002,     
  pages     = '109--134',
  volume  =   '2566', 
  series    = 'Lecture Notes in Computer Science',  
  publisher = 'Springer-Verlag', 
  editor    =  'Torben Mogensen, David Schmidt,  and
                I. Hal Sudburough',
  related =   [(off_home('Tutorial'), 'Companion Web Site')],
  available = ['ps.gz']
]).

bibentry(article,'worst_case_def',
[ author = [genaim,'J.M. Howe',codish],
  title  = 'Worst-Case Groundness Analysis using 
            Definite Boolean Functions',
  journal =  'Theory and Practice of Logic Programming',
  abstract = 'This note illustrates a theoretical worst-case scenario
              for groundness  analyses obtained through abstract
              interpretation over the abstract domain of
              definite Boolean functions. A sequence of
              programs is given for which any Def-based abstract
              interpretation for groundness analysis follows an
              exponential chain.',
  month     = 'September',
  year      = 2001,     
  pages     = '611-615',
  volume  =   '1(5)', 
  available = ['ps.gz']
]).



bibentry(article,'aci_types_full',
[ author  =   [codish,lagoon],      
  title   =    'Type Dependencies for Logic Programs using ACI-unification',
  journal =  'Journal  of Theoretical Computer Science',   
  year    =     2000,    
  volume  =   '238',    
  pages   =    '131-159',
  abstract=  'This paper presents a new notion of typing for logic 
       programs which
       generalizes the notion of directional types.  The generation of
        type dependencies for a logic program is fully
       automatic with respect to a given domain of types.
       The analysis method is based on a novel combination of program
       abstraction and ACI-unification which is shown to be correct and
       optimal. Type dependencies are obtained by abstracting programs,
       replacing concrete terms by their types, and evaluating the meaning
       of the abstract programs using a standard semantics for logic
       programs enhanced by ACI-unification. This approach is generic and
       can be used with any standard semantics. The method is both
       theoretically clean and easy to implement using general purpose
       tools.
       The proposed domain for type analysis is  condensing which
       means that analyses can be carried out in both top-down or
       bottom-up providing analyses with no loss of precision for
       goal-independent analyses.
       The proposed method has been fully implemented within a bottom-up
       approach and the experimental results are promising.',   
  available =   ['ps.gz'],    
  related   =   [ (paper('aci_types:conf'),  'The conference version'),
      (url('http://www.elsevier.nl/gej-ng/10/41/16/172/21/24/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')] 
                 
  ] ).


bibentry(article,'aci_sh_full',
[ author  =     [codish,lagoon, bueno],  
  title   =    'An Algebraic Approach to Sharing Analysis of Logic Programs',
  journal =    'The Journal of Logic Programming',  
  year    =       2000,  
  volume  =     '41',  
  number  =      '2', 
  pages   =      '110-149',
  abstract=     'This paper describes an algebraic approach to the sharing
        analysis of logic programs based on an abstract domain of  set
        logic programs. Set logic programs are logic programs in which
        the terms are sets of variables and unification is based on an
        associative, commutative, and idempotent equality theory.  All of
        the basic operations required for sharing analyses, as well as their
        formal justification, are based on simple algebraic properties of
        set substitutions and set-based atoms. An ordering on set-based
        syntactic objects, similar to ``less general'' on concrete syntactic
        objects, is shown to reflect the notion of ``less sharing''
        information. The (abstract) unification of a pair
        of set-based terms corresponds to finding their most general ACI1
        unifier with respect to this ordering. The unification of a set of
        equations between set-based terms is defined exactly as in the
        concrete case, by solving the equations one by one and repeatedly
        applying their solutions to the remaining equations. We demonstrate
        that all of the operations in a sharing analysis have natural
        definitions which are both correct and optimal.',

  available = ['ps.gz'],  
  related   =   [ (paper('aci_sh:conf'),  'The conference version'),
      (url('http://www.elsevier.nl/gej-ng/10/26/18/57/28/27/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
  ] ).


bibentry(article,'untupling',
[ author  =   [codish, kim, taboch],  
  title   =    'Improving Program Analyses by Structure Untupling',
  journal =  'The Journal of Logic Programming',    
  year    =     2000,    
  volume  =   '43',
  number  =   '3',    
  pages   =    '251-263',    
  abstract=  'It is well-known that adding structural 
        information to an analysis
        domain can increase the precision of the analysis with respect to
        the original domain.  This paper presents a program
        transformation based on untupling and specialisation which can be
        applied to upgrade (logic) program analysis by providing additional
        structural information. It can be applied to (almost) any type of
        analysis and in conjunction with (almost) any analysis framework
        for logic programs.  The approach is an attractive alternative to
        the more complex Pat(R) construction which automatically
        enhances an abstract domain R (in the context of abstract
        interpretation) with structural information.', 
                 
  available =  ['ps.gz'],     
  related=  [(source('untupler.pl'), 'A prototype implementation'),
      (url('http://www.elsevier.nl/gej-ng/10/26/18/59/28/26/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')] 
  ] ).


bibentry(article,'fastmagic',
[ author  =       [codish],
  title   =        'Efficient Goal Directed Bottom-up 
                                     Evaluation of Logic Programs',
  journal =      'The Journal of Logic Programming',
  year    =         1999,
  volume  =       '38',
  number  =       '3',
  pages   =        '354-370',
  abstract=      '  This paper introduces a new strategy for the 
  efficient goal directed
    bottom-up evaluation of logic programs. Instead of combining a
    standard bottom-up evaluation strategy with a Magic-set
    transformation, the evaluation strategy is specialized for the
    application to Magic-set programs which are characterized by clause
    bodies with a high degree of overlapping. The approach is similar to
    other techniques which avoid re-computation by maintaining and
    reusing partial solutions to clause bodies. However, the overhead is
    considerably reduced as these are maintained implicitly by the
    underlying Prolog implementation.  The technique is presented as a
    simple meta-interpreter for goal directed bottom-up evaluation. No
    Magic-set transformation is involved as the dependencies between
    calls and answers are expressed directly within the interpreter. The
    proposed technique has been implemented and shown to provide
    substantial speed-ups in applications of semantic based program
    analysis based on bottom-up evaluation.',
  available =     ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/26/18/30/19/20/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
  ] ).


bibentry(article,'termin',
[ author  =       [codish, taboch],
  title   =        'A Semantic Basis for the Termination  
                  Analysis of Logic Programs',
  journal =      'The Journal of Logic Programming',
  year    =         1999,
  volume  =       '41',
  number  =       '1',
  pages   =        '103-123',
  abstract= 'This paper presents a declarative semantics which
             exhibits the termination properties of a logic
             program. The semantics associates a program with its 
             binary unfoldings --- a possibly infinite set of
             binary clauses. Termination of a program P and goal G
             is indicated by the absence of an infinite chain in the
             binary unfoldings of P starting with G. The main
             contribution is a formal semantic basis for the
             termination analysis of logic programs which facilitates
             both design and implementation. As an implementation
             vehicle we propose a simple meta-interpreter for binary
             unfoldings and the use of an abstract domain based on
             symbolic norm constraints. Many of the recently proposed
             termination analyses for logic programs can be expressed
             concisely within our approach. To demonstrate our
             approach we have reformulated the analysis originally
             described in \cite{LinSag}. The implementation uses a
             standard library for linear equations over the reals. The
             combination of binary unfoldings and a constraint solver
             is shown to significantly simplify the design of the
             analysis.',
  available =     ['ps.gz'],
  related =       [(off_home('TerminWeb'), 'An online implementation'),
                   (paper('termin:conf'), 'The conference version'),
      (url('http://www.elsevier.nl/gej-ng/10/26/18/33/17/20/article.pdf'),
            'PDFfrom the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
  ] ).






bibentry(article,'wpos',
[ author = [heaton, muhamed, codish,amk],     
  title =  'Simple, Efficient and Scalable Groundness 
            Analysis of Logic Programs',          
  journal =   'The Journal of Logic Programming',       
  year =  2000,       
  volume = '45',          
  number = '1-3',          
  pages =  '143-156',          
  abstract=  'The domain of positive Boolean functions, Pos, is by now well
    established for the analysis of the variable dependencies that arise
    within logic programs.  Analyses based on Pos that use binary
    decision diagrams have been shown to be efficient for a wide range of
    practical programs. However, independent of the representation, a
    Pos analysis can never come with any efficiency guarantees because
    of its potential exponential behaviour.  This paper considers
    groundness analysis based on a linear subdomain of Pos. We base a
    goal-dependent groundness analysis for logic programs on this
    subdomain, and show that the resulting precision compares very
    favourably with that of Pos analysis.',        

  available = ['ps.gz'],
  related = 
     [(url('http://www.cs.ukc.ac.uk/people/staff/amk/distribution.tar.uu'),
            'A uuencoded, tar-ed demo implementation'),
      (url('http://www.elsevier.nl/gej-ng/10/26/18/62/25/29/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')
      ]
  ] ).


bibentry(article,'sharing_pos',
[ author = [codish, harald, pjs],       
  title = 'Sharing and
              Groundness Dependencies in Logic Programs',         
  journal =  'ACM
             Transactions on Programming Languages and Systems',      
  year =   1999,      
  volume =  '21',      
  number =  '5',       
  pages =  '948-976',        
  abstract=  'We investigate Jacobs and Langens Sharing domain, 
    introduced for
    the analysis of variable sharing in logic programs, and show that it
    is isomorphic to Marriott and Sondergaards 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 example using reduced order binary decision diagrams, as
    well as efficient implementation of the reduced product, using domain
    factorizations.',      
                 
  available =  ['ps.gz'],
  related = [(paper('coneg:conf'), 'The conference version'),
      (url('http://www.acm.org/pubs/citations/journals/toplas/1999-21-5/p948-codish/'),
            'Abstract from the publisher')]            
  ] ).


bibentry(article,'worstcase',
[ author = [codish],
  title = 'Worst-Case Groundness Analysis using 
              Positive Boolean Functions',         
  journal =  'The Journal of Logic Programming',      
  year =   1999,      
  volume =  '41',       
  number =  '1',       
  pages =  '125--128',        
  abstract=  'This note illustrates a theoretical worst-case 
    scenario for groundness
    analyses obtained through abstract interpretation over the abstract
    domain of positive Boolean functions. A sequence of programs is given
    for which any Pos-based abstract interpretation for groundness
    analysis follows an exponential chain. Another sequence of programs is
    given for which a state-of-the-art implementation based on ROBDDs
    gives a result of exponential size in only three iterations. The moral
    of the story is that a serious Pos analyser must incorporate some
    form of widening to protect itself from the inherent complexity of the
    underlying domain.',      

  available =  ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/26/18/33/17/21/article.pdf'),
            'PDF from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
                 
  ] ).


bibentry(article,'xsb_ai',
[ author = [codish, demoen, kostis],
  title = 'Semantic-Based Program Analysis for 
           Logic-Based Languages using XSB',         
  journal =  'Springer International Journal of Software Tools for
                Technology Transfer',      
  year =   1998,      
  volume =  '2',       
  number =  '1',       
  pages =  '29-45',        
  abstract=  'This paper describes a simple and efficient way of using a logic
    programming language with tabulation for general purpose semantic-based
    program analysis.  The simplicity of the method is based on a clear
    separation of abstraction and control: conceptually, a concrete
    program is executed over an abstract domain and the tabulation
    mechanism avoids recomputation, ensures termination and collects the
    results of the analysis.  The efficiency derives from the fact that an
    abstract interpreter induces an abstract compiler which maps input
    programs to corresponding abstract programs which are (compiled and)
    run in XSB.  The design of new analyses is an easy and fast process,
    because XSB is a general purpose logic programming system which
    supports efficient fix-point computations through tabling implemented
    at the abstract machine level and comes off the shelf: 
    in fact, due to its optimized control and superior tabling
    performance, XSB competitively compares with most of the existing special
    purpose abstract interpretation tools for logic programs.
    We demonstrate that our approach to using XSB for abstract
    interpretation supports the usual optimisations of other frameworks in
    a straightforward and very flexible way.',      
                 
  available =  ['ps.gz'],
  related = [
       (url('http://link.springer.de/link/service/journals/10009/papers/8002001/80020029.pdf'),
            'PDF from the publisher')]
                 
  ] ).


                                           
bibentry(article,'gi_vrs_gd',
[ author = [codish, maria, maurice, herme],       
  title = 'Exploiting Goal Independence in the Analysis of Logic
           Programs',         
  journal =  'The Journal of Logic Programming',      
  year =   1997,      
  volume =  '32',       
  number =  '3',       
  pages =  '247-261',        
  abstract=  'This paper illustrates the use of a top-down 
    framework to obtain goal
    independent analyses of logic programs, a task which is usually
    associated with the bottom-up approach.  While it is well known that
    the bottom-up approach can be used, through the magic set
    transformation, for goal dependent analysis, it is less known that the
    top-down approach can be used for goal independent analysis.  The
    paper describes two ways of doing the latter.
     % and argues that the more efficient approach corresponds closely to
     % the standard bottom-up approach. 
    We show how the results of a goal independent analysis can
    be used to speed up subsequent goal dependent analyses. However this
    speed-up may result in a loss of precision. The influence of domain
    characteristics on this precision is discussed and an experimental
    evaluation using a generic top-down analyzer is described. 
    Our results provide intuition regarding the cases where a two phase
    analysis might be worthwhile.',      
                 
  available =  ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/26/18/47/19/20/abstract.html'),
            'Abstract from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
                 
  ] ).

bibentry(article,'confluent',
[ author = [codish, falaschi, kim, wins],
  title = 'A Confluent Semantic Basis for the Analysis of 
            Concurrent Constraint Logic Programs',         
  journal =  'The Journal of Logic Programming',      
  year =  1997,      
  volume =  '30',       
  number =  '1',       
  pages =  '53-81',        
  abstract=  ' The standard operational semantics of 
    concurrent constraint logic
    languages is not confluent in the sense that different schedulings of
    processes may result in different program behaviors.  While
    implementations are free to choose specific scheduling policies,
    analyses should be correct for all implementations.  Moreover, in the
    presence of parallelism it is usually not possible to determine how
    processes will actually be scheduled.  Efficient program analysis is
    therefore difficult as all process schedulings must be considered.  To
    overcome this problem we introduce a confluent semantics which closely
    approximates the standard (non-confluent) semantics. This semantics
    provides a basis for efficient and accurate program analysis for these
    languages.  To illustrate the usefulness of this approach we sketch
    analyses based on abstract interpretations of the confluent semantics
    which determine if a program is suspension and local suspension free.',      
  available =  ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/26/18/45/17/19/abstract.html'),
            'Abstract from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
                 
  ] ).

bibentry(article,'implications',
[ author = [codish, 'Grigory Mashevitzky'],       
  title = 'Proving Implications by Algebraic Approximation',         
  journal =  'Journal  of Theoretical Computer Science',      
  year =   1996,      
  volume =  '165',       
  pages =  '57-74',        
  abstract=  '  This paper applies techniques of algebraic 
    approximation to provide
    effective algorithms to determine the validity of universally
    quantified implications over lattice structures. We generalize the
    known result which states that any semilattice is approximated in
    the two element lattice.  We show that the validity of a universally
    quantified implication psi over a possibly infinite domain can be
    determined by examining its validity over a simpler domain the size
    of which is related to the number of constants in psi.  Both the
    known as well as the new results have high potential in providing
    practical automated techniques in various areas of application in
    computer science.',      

  available =  ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/41/16/91/17/18/abstract.html'),
            'Abstract from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
                 
  ] ).
                 

bibentry(article,'freeness',
[ author = [codish, dams, file, maurice],       
  title = 'On the Design
  of a Correct Freeness Analysis for Logic Programs',         
  journal =  'The Journal of Logic Programming',      
  year =  1996,      
  volume =  '28',       
  number =  '3',       
  pages =  '181-206',        
  abstract=  '  Several proposals for computing freeness 
  information for
     logic programs have been put forward in recent literature. The
     availability of such information has proven useful in a variety of
     applications, including parallelization of Prolog programs,
     optimizations in Prolog compilers, as well as for improving the
     precision of other analyses.  While these proposals have illustrated
     the importance of such analyses, they lack formal justification.
     Moreover, several have been found incorrect.  This paper introduces
     a novel domain of abstract equation systems describing
     possible sharing and definite freeness of terms in a system of
     equations. A simple and intuitive abstract unification algorithm is
     presented, providing the core of a correct and precise sharing and
     freeness analysis for logic programs. Our contribution is not only a
     correct algorithm, but perhaps primarily, the application of a
     systematic approach in which it is derived by mimicking each step in
     a suitable concrete unification algorithm.  Consequently, the
     abstract algorithm is intuitive --- as it resembles the concrete
     algorithm. It is amenable to formal justification --- as the proof
     of correctness boils down to showing that each step in the concrete
     algorithm is mimicked by a corresponding step in the abstract
     algorithm. Finally, it is precise --- as each step mimics only those
     situations which can arise in the concrete algorithm.',      
                 
  available =  [],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/26/18/42/19/17/abstract.html'),
            'Abstract from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')]
                 
  ] ).

bibentry(article,'magicwand',
[ author = [codish, demoen],       
  title = 'Analysing Logic Programs using "Prop"-ositional 
           Logic Programs and a Magic Wand',         
  journal =  'The Journal of Logic Programming',      
  year =   1995,      
  volume =  '25',       
  number =  '3',       
  pages =  '249-274',        
  abstract=  'This paper illustrates the role of a class of 
 ``prop''-ositional logic
   programs in the analysis of complex properties of logic programs.
   Analyses are performed by abstracting Prolog programs to corresponding
   ``prop''-ositional logic programs which approximate the original
   programs and have finite meanings.  We focus on a groundness analysis
   which is equivalent to that obtained by abstract interpretation using
   the domain Prop. The main contribution is in the ease in which a
   highly efficient implementation of the analysis is obtained. The
   implementation is bottom-up and provides approximations of a programs
    success patterns.  Goal dependent information such as
   call patterns is obtained using a magic-set transformation. A novel
   compositional approach is applied so that call patterns for arbitrary
   goals are derived in a precise and efficient way.',      

  available =  ['ps.gz'],    
  related =    [(paper('magicwand:conf'),'The conference version'),
      (url('http://www.elsevier.nl/gej-ng/10/26/18/36/17/18/abstract.html'),
            'Abstract from the publisher'),
      (url('http://scirus.com/ausearch?author=Codish'),
            'PDF from Scirus - scientific search engine')
             ]  
                 
  ] ).




bibentry(article,'oracle',
[ author = [barbuti,  codish, giaco, 'Michael Maher'],       
  title = 'Oracle Semantics for Prolog',         
  journal =  'Information and Computation',      
  year =   1995,      
  volume =  '22',       
  number =  '2',       
  pages =  '178-200',        
  abstract=  'This paper proposes to specify semantic definitions for logic
     programming languages such as Prolog in terms of an oracle which
     specifies the control strategy and identifies which clauses are to be
     applied to resolve a given goal. The approach is quite general. It is
     applicable to Prolog to specify both operational and declarative
     semantics as well as other logic programming languages.

     Previous semantic definitions for Prolog typically encode the
     sequential depth-first search of the language into various
     mathematical frameworks. Such semantics mimic a Prolog interpreter in
     the sense that following the ``leftmost'' infinite path in the
     computation tree excludes computation to the right of this path from
     being considered by the semantics.
     %
     The basic idea in this paper is to abstract away from the sequential
     control of Prolog and to provide a declarative characterization of the
     clauses to apply to a given goal.  The decision whether or not to
     apply a clause is viewed as a query to an oracle which is specified
     from within the semantics and reasoned about from outside.  This
     approach results in simple and concise semantic definitions which are
     more useful for arguing the correctness of program transformations and
     providing the basis for abstract interpretations than previous
     proposals.',      
                 
  available =  ['ps.gz'],    
  related =    [(paper('oracle:conf'),'The conference version'),
      (url('http://theory.lcs.mit.edu/~iandc/References/barbuticgm1995:178.html'),
            'Abstract from the journal homepage')]  
                 
  ] ).


bibentry(article,'combining',
[ author = [codish, 'Anne Mulkers', maurice, maria, herme],
  title = 'Improving Abstract Interpretations by Combining
            Domains',         
  journal =  'ACM Transactions on Programming Languages and Systems',      
  year =   1995,      
  volume =  '17',       
  number =  '1',       
  pages =  '28-44',        
  abstract=  'Static analysis based on abstract interpretation of 
    logic programs
    over combined domains is considered. It is known that analyses over
    combined domains potentially provide more information than obtained by
    the independent analyses. However, the construction of a combined
    analysis often requires redefining the basic operations for the
    combined domain. A practical approach to maintain precision in
    combined analyses of logic programs which reuses the individual
    analyses and does not redefine the basic operations is illustrated.
    The advantage of the approach is that proofs of correctness for the
    new domains are not required and implementations can be reused. The
    approach is demonstrated by showing that a combined sharing analysis
    --- constructed from ``old'' proposals --- compares well with other
    ``new'' proposals suggested in recent literature both from the point
    of view of efficiency and accuracy.',      
                 
  available =  ['ps.gz'],    
  related =    [(paper('combining:conf'),'The conference version'),
      (url('http://www.acm.org/pubs/citations/journals/toplas/1995-17-1/p28-codish/'),
            'Abstract from the publisher')]  
                 
  ] ).

bibentry(article,'bot-up',
[ author  =   [ codish, dams,  yardeni],    
  title   =    'Bottom-Up Abstract Interpretation of Logic Programs',
  journal =  'Journal of Theoretical Computer Science',
  publisher =    'Elsevier Science Publishers',
  year    =     1994,
  volume  =   '124',
  pages   =    '93--125',   
  abstract=  'This paper presents a formal framework for the bottom-up abstract
     interpretation of logic programs which can be applied to approximate
     answer substitutions, partial answer substitutions and
      call patterns for a given program and arbitrary initial goal.
     The framework is based on a T_P like semantics defined over a
     Herbrand universe with variables which has previously been shown to
     determine the answer substitutions for arbitrary initial goals.  The
     first part of the paper reconstructs this semantics to provide a more
     adequate basis for abstract interpretation.  A notion of  abstract
     substitution is introduced and shown to determine an abstract
     semantic function which for a given program can be applied to
     approximate the answer substitutions for an arbitrary initial goal.

     The second part of the paper extends the bottom-up approach to provide
     approximations of both partial answer substitutions and call patterns.
     This is achieved by applying Magic Sets and other existing
     techniques to transform a program in such a way that the answer
     substitutions of the transformed program correspond to the partial
     answer substitutions and call patterns of the original program. This
     facilitates the analysis of concurrent logic programs (ignoring
     synchronization) and provides a collecting semantics which
     characterizes both success and call patterns.',
                 
  available =  ['ps.gz'],
  related = [
       (url('http://www.elsevier.nl/gej-ng/10/41/16/50/17/20/abstract.html'),
            'Abstract from the publisher')]
% Reviewed in {\it Computing Reviews\/} 36(3):166, The ACM Press, March
% 1995.                  
  ] ).                                          


bibentry(article,'suspension',
[ author = [codish,  falaschi, kim],      
  title =  'Suspension Analysis for Concurrent Logic Programs',
  journal = 'ACM Transactions on Programming Languages and Systems',
  year =    1994,
  volume =  '16',
  number =  '3',
  pages =    '649-686',   
  abstract=  'Concurrent logic languages specify reactive systems which 
     consist of
     collections of communicating processes. The presence of unintended
     suspended computations is a common programming error which is
     difficult to detect using standard debugging and testing techniques.
     We develop a number of analyses, based on abstract interpretation,
     which succeed if a program is definitely suspension free.  If an
     analysis fails the program may, or may not, be suspension free.
     Examples demonstrate that the analyses are practically useful.  They
     are conceptually simple and easy to justify because they are based
     directly on the transition system semantics of concurrent logic
     programs. A naive analysis must consider all scheduling
     policies. However, it is proven that for our analyses it suffices to
     consider only one scheduling policy, allowing for efficient
     implementation.',    
                 
  available =    ['ps.gz'], 
  related =      [(paper('suspension:conf'),'The conference version'),
      (url('http://www.acm.org/pubs/citations/journals/toplas/1994-16-3/p649-codish/'),
            'Abstract from the publisher')]
%   Reviewed in {\it Computing Reviews\/} 36(8):436, The ACM Press, March
%   1995.               
  ] ).


bibentry(article,'modelling',
[ author =  [barbuti,  codish, giaco, levi],     
  title =   'Modelling Prolog Control',
  journal = 'Journal of Logic and Computation',
  year =     1993,
  volume =   '3',   
  pages =    '579--603',     
  abstract=    'The goal of this paper is to construct a semantic basis for the
      abstract interpretation of Prolog programs. Prolog is a well-known
      logic programming language which applies a depth-first search strategy 
      in order to provide a practical approximation of Horn clause logic.
      While pure logic programming has clean fixpoint, model-theoretic and
      operational semantics the situation for Prolog is different. 
      Difficulties in capturing the declarative meaning of Prolog programs 
      have led to various semantic definitions which attempt to encode the 
      search strategy in different mathematical frameworks. However semantic 
      based analyses of Prolog are typically achieved by abstracting the more 
      simple but less precise declarative semantics of pure logic Programs.

      We propose instead to model Prolog control in a simple constraint logic
      language which is presented together with its declarative and operational
      semantics. This enables us to maintain the usual approach to declarative 
      semantics of logic programs while capturing control aspects such as 
      search strategy and selection rule.',
  available = ['ps.gz'],      
  related =   [(paper('modelling:conf'),'The conference version')]
  ] ).

bibentry(article,'specialising',
  [ author =  [john,  codish,  udi],     
    title =   'Specialising Prolog and FCP Programs Using Abstract
               Interpretation',     
    journal =  'Journal of New Generation Computing',    
    year =     1988,    
    volume =   '6',    
    pages =    '159--186',    

    available = []
    ] ).  


bibentry(article,'or2and',
[ author = [codish, udi],      
  title =  'Compiling OR-parallelism into AND-parallelism',     
  journal =  'Journal of New Generation Computing',    
  year =    1987,     
  volume =  '5',   
  pages =  '45--61',      
  available = [],    
  related =  [(paper('or2and:conf'),'The conference version')]    
  ] ).



bibentry(article,'pressing',
[ author = ['Leon Sterling', codish],      
  title =  'Pressing for Parallelism; a Prolog Program Made Concurrent',   
  journal = 'Journal of Logic Programming',
  year =   1986,      
  volume = '3',      
  number = '1',      
  pages =  '75--94', 
  available = []
  ] ).

%%% CONFERENCE PAPERS  


/*

bibentry(,inproceedings'',
[ author    = '',   
  title     = '',       
  abstract  = '', 
  booktitle = '',       
  volume    = '',       
  series    = '',      
  publisher = '',   
  pages     = '',       
  year      = ,
  month     = '',       
  available = [],  
  related   =  [('', 'The journal version')]
]).

*/

bibentry(inproceedings,'and2or:conf',
[ author    = [codish, udi],   
  title     = 'Compiling OR-parallelism into
               AND-parallelism',        
  abstract  = ' ', 
  booktitle = 'Proceedings of the Third International Conference
               on Logic Programming',   
  volume    = '225',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '283--297',       
  year      = 1986,
  month     = ' ',
  address   =  'London',
  related =  [(paper('or2and'),'The journal version')], 
  available = []
]).


bibentry(inproceedings,'fullabstract:conf',
[ author    = ['Rob Gerth', codish, 'Yossi Lichtenstein',udi],   
  title     = 'Fully Abstract Denotational Semantics for 
                Concurrent Prolog',     
  abstract  = ' ', 
  booktitle = 'Proceedings of the Third Annual Symposium on 
               Logic in Computer Science',      
  volume    = ' ',       
  series    = ' ',      
  publisher = 'IEEE Computer Society',   
  pages     = '320--333',       
  year      = 1988,
  month     = 'July',   
  address   = 'Edinburgh, Scotland',
  available = []
]).


bibentry(inproceedings,'safe_approx:conf',
[ author    = [codish, john, udi],   
  title     = 'Using Safe Approximations
               of Fixed Points for Analysis of Logic Programs',         
  abstract  = ' ', 
  booktitle = 'Meta-programming in Logic Programming',  
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT press',   
  pages     = '233--262',       
  year      = 1989,     
  month     = ' ',      
  available = []
]).



bibentry(inproceedings,'msg_prot:conf',
[ author    = [ codish,  dams,udi],   
  title     = 'Automatic Detection of Incomplete
               Message Protocols in Concurrent Logic Programs',         
  abstract  = ' ', 
  booktitle = 'Proceedings of the
               Meta 90 workshop on meta-programming in logic',  
  volume    = ' ',       
  series    = ' ',      
  publisher = ' ',   
  pages     = '?',       
  year      = 1990,     
  month     = ' ',      
  available = []
]).


bibentry(inproceedings,'pair_share:conf',
[ author    = [codish,  dams,  yardeni],   
  title     = 'Derivation and Safety of an Abstract Unification 
                 Algorithm for Groundness and Aliasing Analysis',       
  abstract  = ' ', 
  booktitle = 'Proceedings of the Eighth International Conference on Logic
                Programming',   
  editor    =    'Furukawa, K.',
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT Press',   
  pages     = '79--93',       
  year      = 1991,     
  month     = ' ',
  address   = 'Paris, France',
  available = []
]).


bibentry(inproceedings,'susp:conf',
[ author    = [codish, falaschi, kim],   
  title     = 'Suspension Analysis for Concurrent Logic Programs',      
  abstract  = ' ', 
  booktitle = 'Proceedings of the Eighth International
                Conference on Logic Programming',       
  editor    = 'Furukawa, K.',
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT Press',   
  pages     = '331--345',       
  year      = 1991,     
  month     = ' ',
  address   = 'Paris, France',  
  available = [], 
  related =      [(paper('suspension'),'The journal version')]
]).

bibentry(inproceedings,'modelling:conf',
[ author    = [barbuti, codish, giaco, levi],   
  title     = 'Modelling Prolog Control',       
  abstract  = ' ', 
  booktitle = 'Proceedings of the Nineteenth ACM symposium on
                 Principles of Programming Languages',  
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The ACM Press',   
  pages     = '95--104',       
  year      = 1992,     
  month     = 'January',        
  available = [], 
  related =      [(paper('modelling'),'The journal version')]
]).



bibentry(inproceedings,'oracle:conf',
[ author    = [barbuti, codish, giaco, maher],   
  title     = 'Oracle Semantics for Prolog',    
  abstract  = ' ', 
  booktitle = 'Proceedings of the Third International
                 Conference on Algebraic and Logic Programming',        
  volume    = '632',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '100-114',       
  year      = 1992,     
  month     = 'September',
  address   = 'Volterra, Italy',        
  available = [ ], 
  related =      [(paper('oracle'),'The journal version')]
]).


bibentry(inproceedings,'compositional:conf',
[ author    = [codish, debray,giaco],   
  title     = 'Compositional Analysis of Modular Logic Programs',       
  abstract  = ' ', 
  booktitle = 'Proceedings of the Twentieth ACM symposium
                on Principles of Programming Languages',        
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The ACM Press',   
  pages     = '451--464',       
  year      = 1993,     
  month     = ' ',      
  available = [ ]
]).


bibentry(inproceedings,'combining:conf',
[ author    = [codish, 'A. Mulkers', maurice, maria,herme],
  title     = 'Improving Abstract Interpretations by Combining
               Domains',        
  abstract  = ' ', 
  booktitle = 'Proceedings of the ACM Symposium on Partial Evaluation and
               Semantics-Based Program Manipulation',   
  volume    = ' ',       
  series    = ' ',      
  publisher = 'ACM Press',   
  pages     = '194--205',       
  year      = 1993,     
  month     = 'June',   
  available = [ ], 
  related =      [(paper('combining'),'The journal version')]
]).



bibentry(inproceedings,'lsusp:conf',
[ author    = [codish, falaschi,kim,wins],   
  title     = 'Efficient Analysis of Reactive Properties of 
               Concurrent Constraint Logic Programs',   
  abstract  = ' ', 
  booktitle = 'Proceedings of the Twentieth International Colloquium on
                Automata, Languages and Programming',   
  volume    = ' ',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = ' ',   
  pages     = ' ',       
  year      = 1993,     
  month     = 'July',   
  available = [], 
  related =      [(paper('confluent'),'The journal version')]
]).


bibentry(inproceedings,'freeness_and_correctness:conf',
[ author    = [codish, dams, file,maurice],   
  title     = 'Freeness Analysis for Logic Programs --- 
               And Correctness ?',      
  abstract  = ' ', 
  booktitle = 'Proceedings of the Tenth International Conference on Logic
               Programming',
  editor    = 'Warren, David S.',       
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT Press',   
  pages     = '116--134',       
  year      = 1993,     
  month     = ' ',
  address   = 'Budapest, Hungary',
  isbn      = '0-262-73105-3',  
  available = []
]).


bibentry(inproceedings,'freeness_and_num:conf',
[ author    = ['V. Dumortier, G. Janssens', maurice, codish],   
  title     = 'Freeness Analysis in the Presence of 
                Numerical Constraints',         
  abstract  = ' ', 
  booktitle = 'Proceedings of
               the Tenth International Conference on Logic Programming',
  editor    = 'Warren, David S.',
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT Press',   
  pages     = '100-115',       
  year      = 1993,     
  month     = ' ',
  address   = 'Budapest, Hungary',
  isbn      = '0-262-73105-3',
  available = []
]).



bibentry(inproceedings,'freeness_shlin:conf',
[ author    = [maurice,codish],
  title     = 'Freeness, Sharing, Linearity and
               Correctness --- All at Once',    
  abstract  = ' ', 
  booktitle = 'Proceedings of the 1993 International
                Workshop on Static Analysis',   
  volume    = ' ',       
  series    = ' ',      
  publisher = ' ',   
  pages     = '?',       
  year      = 1993,     
  month     = ' ',      
  available = []
]).


bibentry(inproceedings,'magicwand:conf',
[ author    = [codish, demoen],   
  title     = 'Analysing Logic Programs using 
               Prop-ositional Logic Programs and a Magic Wand',         
  abstract  = ' ', 
  booktitle = 'Proceedings of the
         1993 International Logic Programming Symposium',       
  editor    = 'Miller, Dale',
  volume    = ' ',       
  series    = ' ',      
  publisher = 'The MIT Press',   
  pages     = '114--129',       
  year      = 1993,     
  month     = ' ',      
  available = [], 
  related =      [(paper('magicwand'),'The journal version')]
]).



bibentry(inproceedings,'gi_vrs_gd:conf',
[ author    = [codish,maria, maurice, herme],   
  title     = 'Goal Dependent vs Goal Independent Analysis of Logic
               Programs',       
  abstract  = ' ', 
  booktitle = 'Proceedings of the Fifth International Conference on Logic
               Programming and Automated Reasoning',    
  volume    = '822',       
  series    = 'Lecture Notes in Artificial Intelligence',      
  publisher = 'Springer-Verlag',   
  pages     = '305--320',       
  year      = 1994,     
  month     = 'July',   
  address   = 'Kiev, Ukraine',
  available = [], 
  related =      [(paper('gi_vrs_gd'),'The journal version')]
]).


bibentry(inproceedings,'multiple_incar:conf',
[ author    = [codish, demoen],   
  title     = 'Deriving Polymorphic Type Dependencies 
       for Logic Programs Using Multiple  Incarnations of Prop',        
  abstract  = ' ', 
  booktitle = 'Proceedings of the First Static Analysis Symposium',     
  volume    = '864',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '281-297',       
  year      = 1994,     
  month     = 'September',      
  available = [], 
  related =      [(paper('aci_types_full'),'Subsequent work on types')]
]).


bibentry(inproceedings,'alp94:conf',
[ author =  [codish, 'Grigory Mashevitzky'] ,
  title =        'Proving Implications by Algebraic Approximation' ,
  abstract =  'This paper applies techniques of algebraic approximation
          to provide effective algorithms to determine the validity of
          universally quantified implications over lattice
          structures. We generalize the known result which states that
          any semilattice is approximated in the two element
          lattice. We show that the validity of a universally
          quantified implication psi over a possibly infinite
          domain can be determined by examining its validity over a
          simpler domain the size of which is related to the number of
          constants in psi. Both the known as well as the new
          results have high potential in providing practical automated
          techniques in various areas of application in computer
          science.',
  booktitle =    'Proceedingss of the 4th International
                  Conference on Algebraic and Logic Programming',
  volume =        '850',
  series =        'Lecture Notes in Computer Science',
  publisher =     'Springer-Verlag',
  pages =         '6-22',
  year =         1994,
  month =        'September',
  available =      [],
  related =        [(paper('aa-tcs'), 'The journal version')]
]).

bibentry(inproceedings,'key_step',
[ author    = 'M. Bruynooghe, M. Codish, A. Mulkers',   
  title     = 'Abstracting Unification:
               A Key Step in the Design of Logic Program Analyses',     
  abstract  = ' ', 
  booktitle = 'Computer Science Today',
  editor    = 'Jan van Leeuwen',        
  volume    = '1000',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '406--425',       
  year      = 1995,     
  month     = ' ',      
  available = []
]).

bibentry(inproceedings,'aci_types:conf',
[ author    = [codish, lagoon],   
  title     = 'Type Dependencies for Logic Programs
               using ACI-unification',  
  abstract  = ' ', 
  booktitle = 'Proceedings of the 1996 Israeli Symposium
               on Theory of Computing and Systems',     
  volume    = ' ',       
  series    = ' ',      
  publisher = 'IEEE Press',   
  pages     = '136-145',       
  year      = 1996,     
  month     = 'June',   
  available = [], 
  related =      [(paper('aci_types_full'),'The journal version')]
]).

bibentry(inproceedings,'aci_sh:conf',
[ author    = [codish,lagoon, bueno],   
  title     = 'An Algebraic Approach to
       Sharing Analysis of Logic Programs',     
  abstract  = ' ', 
  booktitle = 'Proceedings of the 
       Fourth International Static Analysis Symposium', 
  volume    = '1302',       
  series    = 'LNCS',      
  publisher = 'Springer-Verlag',   
  pages     = '68--82',       
  year      = 1997,     
  month     = ' ',      
  available = [], 
  related =      [(paper('aci_sh_full'),'The journal version')]
]).


bibentry(inproceedings,'termin:conf',
[ author    = [codish, taboch],   
  title     = 'A Semantic Basis for Termination
       Analysis of Logic Programs and its Realization using Symbolic
       Norm Constraints',       
  abstract  = ' ', 
  booktitle = 'Proceedings of the Sixth International
       Conference on Algebraic and Logic Programming',  
  volume    = '1298',       
  series    = 'LNCS',      
  publisher = 'Springer-Verlag',   
  pages     = '31-45',       
  year      = 1997,     
  month     = 'September',      
  available = [], 
  related =      [(paper('termin'),'The journal version')]
]).


bibentry(inproceedings,'coneg:conf',
[ author    = [codish,harald],
  title     = 'The Boolean Logic of Set Sharing Analysis',     
  abstract = "We show that Jacobs and Langen's domain for set-sharing
          analysis is isomorphic to the domain of positive Boolean
          functions, introduced by Marriott and Søndergaard for
          groundness dependency analysis. Viewing a set-sharing
          description as a minterm representation of a Boolean
          function leads to re-casting sharing analysis as an
          instantiation dependency analysis. The key idea is to view
          the sets of variables in a sharing domain element as the
          models of a Boolean function. In this way, sharing sets are
          precisely dual negated positive Boolean functions. This new
          view improves our understanding of sharing analysis
          considerably and opens up new avenues for the efficient
          implementation of this kind of analysis, for example using
          ROBDDs. To this end we express Jacobs and Langen's abstract
          operations for set sharing in logical form.",
  booktitle = 'Principles of Declarative Programming',  
  volume    = '1490',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '89--101',       
  year      = 1998,     
  month     = 'September',      
  available = [], 
  related =      [(paper('sharing_pos'),'The journal version'),
   (url('http://link.springer.de/link/service/series/0558/tocs/t1490.htm'),
                  'PDF from Springer')]
]).


bibentry(inproceedings,'incr:conf',
[ author    = [genaim, codish],   
  title     = 'Incremental Refinement of Semantic Based
        Program Analysis for Logic Programs',   
  abstract  = ' ', 
  booktitle = 'Proceedings of the 22nd
        Australasian Computer Science Conference',      
  volume    = ' ',       
  series    = ' ',      
  publisher = 'Springer-Verlag',   
  pages     = '?',       
  year      = 1999,     
  month     = 'January',        
  available = []
]).

bibentry(inproceedings,'aci-def:conf',
[ author    = [genaim, codish],   
  title     = 'The Def-inite Approach to Dependency Analysis',  
  abstract = 'We propose a new representation for the domain of
               Definite Boolean functions. The key idea is to view the
               set of models of a Boolean function as an incidence
               relation between variables and models. This enables two
               dual representations: the usual one, in terms of
               models, specifying which variables they contain; and
               the other in terms of variables, specifying which
               models contain them.  We adopt the dual representation
               which provides a clean theoretical basis for the
               definition of efficient operations on Def in terms
               of classic ACI1 unification theory.  Our approach
               illustrates in an interesting way the relation of
               Def to the well-known set-Sharing domain which
               can also be represented in terms of sets of models and
               ACI1 unification.  From the practical side, a prototype
               implementation provides promising results which
               indicate that this representation supports efficient
               groundness analysis using Def formula.', 
  booktitle =  'Presented at the APPIA-GULP-PRODE 2000
                Joint Conference on Declarative Programming (La Habana)', 
  volume =     ' ', 
  series = ' ', 
  publisher = '', 
  pages = '?', 
  year = 2000, 
  month = 'December', 
  available = ['ps.gz']
]).

bibentry(inproceedings,'aci-def:conf2',
[ author    = [genaim, codish],   
  title     = 'The Def-inite Approach to Dependency Analysis',  
  abstract = 'We propose a new representation for the domain of
               Definite Boolean functions. The key idea is to view the
               set of models of a Boolean function as an incidence
               relation between variables and models. This enables two
               dual representations: the usual one, in terms of
               models, specifying which variables they contain; and
               the other in terms of variables, specifying which
               models contain them.  We adopt the dual representation
               which provides a clean theoretical basis for the
               definition of efficient operations on Def in terms
               of classic ACI1 unification theory.  Our approach
               illustrates in an interesting way the relation of
               Def to the well-known set-Sharing domain which
               can also be represented in terms of sets of models and
               ACI1 unification.  From the practical side, a prototype
               implementation provides promising results which
               indicate that this representation supports efficient
               groundness analysis using Def formula.', 
  booktitle =  'Proceedings of the 10th European Symposium On Programming', 
  volume =     '2028', 
  series = 'Lecture Notes in Computer Science', 
  publisher = 'Springer-Verlag', 
  pages = '417--431', 
  year = 2001, 
  month = 'April', 
  related =      [(paper('aci-def:conf'),'An earlier version'),
   (url('http://link.springer.de/link/service/series/0558/tocs/t2028.htm'),
                  'PDF from Springer')],
  available = []
]).

bibentry(inproceedings, 'TypedPos',
[ author = [maurice,wim,codish],
  title  = 'POS(T): Analyzing Dependencies in Typed Logic Programs',

  abstract = 'Dependencies play a major role in the analysis of program
  properties. The analysis of groundness dependencies for logic
  programs using the class of positive Boolean functions is a
  main applications area. Work has been done to improve its precision
  through the integration of either pattern information or type
  information. This paper develops another approach where type
  information is exploited. Different from previous work, a separate
  simple analysis is done for each subtype of the types. Also, a
  technique is developed that reuses the results of a polymorphic
  predicate for the type instances under which it is called.',

  booktitle =  'Perspectives of System
        Informatics, 4th International Andrei Ershov Memorial
        Conference, (PSI)',
  volume =     '2244', 
  series = 'Lecture Notes in Computer Science', 
  publisher = 'Springer-Verlag', 
  pages = '406--420', 
  year = 2001, 
  month = 'July',
  available = ['ps.gz']
]).


bibentry(inproceedings,'lpos',
[ author    = [codish,genaim,harald,pjs],   
  title     = 'Higher-Precision Groundness Analysis',       
  abstract  = 'Groundness analysis of logic programs using Pos-based 
  abstract interpretation is one of the clear success stories of the last
  decade in the area of logic program analysis. In this work we
  identify two problems with the Pos domain, the multiplicity and
  sign problems, that arise independently in groundness and uniqueness
  analysis. We describe how these problems can be solved using an
  analysis based on a domain Size for inferring term size relations.
  However this solution has its
  own shortcomings because it involves a widening operator which leads
  to a loss of Pos information. Inspired by Pos, Size and the
  LSign domain for abstract linear arithmetic constraints we
  introduce a new domain LPos, and show how it can be used for
  groundness and uniqueness analysis. The idea is to use the sign
  information of LSign to improve the widening of Size so that
  it does not lose Pos information. We prove that the resulting analyses
  using LPos are uniformly more precise than those using Pos.', 
  booktitle = 'Proceedings of the Seventeenth International 
               Conference on Logic Programming',        
  volume    = '2237',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '135--149',       
  year      = 2001,
  month     = 'December',       
  available = [],  
  related=  [(source('lpos.ps.gz'), 'technical report version')] 
]).


bibentry(inproceedings,'lpar01',
[ author = [genaim,codish],
  title  = 'Inferring Termination Conditions for Logic  
        Programs using Backwards Analysis',

  abstract = 'This paper focuses on the inference of modes for which a
    logic program is guaranteed to terminate. This generalizes traditional
    termination analysis where an analyzer tries to verify termination for
    a specified mode.  The contribution is a methodology which combines
    traditional termination analysis and backwards analysis to obtain
    termination inference.  This leads to a better understanding of
    termination inference, simplifies its formal justification, and
    facilitates implementation.  We evaluate the application of this
    approach to enhance an existing termination analyzer to perform also
    termination inference.',

  booktitle = 'Proceedings of the Eighth International Conference 
               on Logic for Programming, 
               Artificial Intelligence and Reasoning',     
  editor    = 'Nieuwenhuis, R. and Voronkov, A.',
  volume    = '2250',       
  series    = 'Lecture Notes in Artificial Intelligence',      
  publisher = 'Springer-Verlag',   
  pages     = '681--690',       
  year      = 2001,
  month     = 'December',       
  related =      [ (source('ba_term.ps.gz'), 'technical report version'),
                   (off_home('TerminWeb'), 'An online implementation'),
                   (paper('termin'), 'A paper on Termination Analysis')],
  available = ['ps']
]).

bibentry(inproceedings,'vmcai02',
[ author    = [genaim,codish,john,lagoon], 
  title     = 'Combining Norms to Prove Termination',   
  abstract = 'Automatic termination analysers typically measure the
    size of terms applying norms which are mappings from terms to the
    natural numbers. This paper illustrates how to enable the use of
    size functions defined as tuples of these simpler norm functions.
    This approach enables us to simplify the problem of deriving
    automatically a candidate norm with which to prove
    termination. Instead of deriving a single, complex norm function,
    it is sufficient to determine a collection of simpler norms, some
    combination of which, leads to a proof of termination.  We propose
    that a collection of simple norms, one for each of the recursive
    data-types in the program, is often a suitable choice.  We first
    demonstrate the power of combining norm functions and then the
    adequacy of combining norms based on regular-types.  ',
  booktitle = 'Third International
        Workshop on Verification, Model Checking and Abstract
        Interpretation',       
  editor    = 'Agostino Cortesi',
  volume    = '2294',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '126--138',       
  year      = 2002,
  month     = 'January',       
  available = [ps],  
  related   =  []
]).


bibentry(inproceedings,'sas02',
[ author    = [maurice,codish,genaim,wim], 
  title     = 'Reuse of Results in Termination Analysis of 
               Typed Logic Programs',    
  abstract = 'Recent works by the authors address the problem of 
          automating the
          selection of a candidate norm for the purpose of termination
          analysis. These works illustrate a powerful technique in which a
          collection of simple type-based norms --- one for each data type in
          the program --- are combined together to provide the candidate norm.

          The current paper extends these results by investigating type
          polymorphism. We show that by considering polymorphic types we 
          reduce,
          without sacrificing precision, the number of type-based norms which
          should be combined to provide the candidate norm.
          Moreover, we show that when a generic polymorphic typed program
          component occurs in one or more specific type contexts, we need not
          reanalyse it. All of the information concerning its termination and
          its effect on the termination of other predicates in that context can
          be derived directly from the context independent analysis of that
          component based on norms derived from the polymorphic types.',
  booktitle = 'Proceedings of The 9th International Static Analysis 
               Symposium (SAS 2002 - to appear)',       
  editor    = 'Manuel Hermenegildo and Germán Puebla',
  volume    = '2477',       
  series    = 'Lecture Notes in Computer Science',      
  publisher = 'Springer-Verlag',   
  pages     = '477-492',       
  year      = 2002,
  month     = 'September',       
  available = [],  
  related   =  []
]).


bibentry(inproceedings,'loopBYloop',
    [ author = [codish,genaim,maurice,john,wim],
      title = 'One Loop at a Time',
      abstract =   
       'Classic techniques for proving termination require the
       identification of a measure mapping program states to the
       elements of a well founded domain and to show that this measure
       decreases with each iteration of a loop in the program. This is
       a global termination condition --- there is a single
       measure which must be shown to decrease over all of the loops
       in the program. In this note we look at systems based on
       local termination conditions which allow the involvement
       of different well founded domains and termination measures for
       different loops in the program.  We illustrate the practical
       advantages of applying local criteria in automated termination
       proving systems and demonstrate how Ramsey Theorem clarifies
       their formal justification.',
  booktitle = '6th International Workshop on Termination (WST 2003)',
  year      = 2003,     
  month     = 'June',
  available = ['ps']
]).



bibentry(inproceedings,'wlpe03',
    [ author = [codish,genaim],
      title = 'Proving Termination One Loop at a Time',
      abstract = 'Classic techniques for proving termination require
       the identification of a measure that maps program states to the
       elements of a well-founded domain. Termination is guaranteed if
       this measure is shown to decrease with each iteration of a loop
       in the program. This is a \emph{global} termination condition
       --- there exists a measure which is shown to decrease over all
       of the loops in the program.  In recent years, systems based on
       \emph{local} termination conditions are emerging. Here,
       termination is guaranteed if for every loop there exists a
       measure which decreases as execution follows through that loop.
       In this paper we question the relationship between the two
       approaches. Reasoning locally is more convenient. But is the
       local approach really more powerful?  We show that for a large
       class of termination problems the two approaches are equally
       powerful. To this end we demonstrate that given local
       conditions which support a proof of termination, a
       corresponding global condition can always be constructed. On
       the one hand, the local conditions are simpler and easier to
       find. Yet on the other hand, in the local approach one must
       consider a closure operation on loops which may require to
       consider an exponential number of local conditions.  ',
  booktitle = 'The 13th Workshop on Logic Programming Environments',
  year      = 2003,     
  month     = 'December',
  available = ['ps']
]).

bibentry(inproceedings,'wst04',
    [ author = ['Lior Tamary',codish],
      title = 'Abstract Partial Evaluation for Termination Analysis',
      abstract = ' Current techniques for proving termination of logic
       programs focus on size and instantiation information. Structure
       information is ignored and for many examples this leads to
       imprecision in the analysis.  There are two approaches to
       consider structure information: either to enhance the abstract
       domain over which the analysis is performed; or to transform
       the program so that structure in the concrete program is
       considered before abstract interpretation is applied.  In
       \cite{adornments-lopstr03}, the authors propose a technique to
       transform a program so that the predicate names are adorned to
       reflect different structure patterns. In this approach, the
       adorned program is equivalent to the original program and
       termination analysis of the adorned program is more precise.

      In this paper we present an alternative approach based on
      well-studied techniques of partial evaluation (unfolding) and
      abstract interpretation. Partial evaluation is a natural choice
      when the intention is to pre-evaluate just so much as to
      consider the structure present in the program. The advantage of
      this approach is that it relies completely on well-studied
      formal techniques.

      In addition to partial evaluation we also abstract the program,
      maintaining structure, but possibly adding computations. This
      process preserves nontermination and hence is safe for
      termination analysis.  This often simplifies the transformation.

      We obtain results similar to those illustrated in
      \cite{adornments-lopstr03}. We also compare our results to those
      obtained using ECCE \cite{ecce} which is an off-the-shelf
      partial evaluator. Our results are more precise and analyses are
      considerably faster than those obtained using ECCE.  ',
  booktitle = '7th International Workshop on Termination (WST 2004)',
  year      = 2004,     
  month     = 'June',
  available = ['ps']
]).

bibentry(inproceedings,'iclp05',
[ author    = [codish,lagoon,pjs],
  title     = 'Testing for Termination with Monotonicity Constraints',
  abstract  = 'Termination analysis is often performed over the
abstract domains of  
monotonicity constraints or of size change graphs. First, the
transition relation for a given program is approximated by a set of
descriptions. Then, this set is closed under a composition
operation. Finally, termination is determined if all of the idempotent
loop descriptions in this closure have (possibly different) ranking
functions.
This approach is complete for size change graphs: An idempotent loop
description has a ranking function if and only if it has one which
indicates that some specific argument decreases in size.
In this paper we generalize the size change criteria for size change
graphs which are not idempotent.
We also illustrate that proving termination with monotonicity
constraints is more powerful than with size change graphs and
demonstrate that the size change criteria is incomplete for
monotonicity constraints. Finally, we provide a complete termination
test for monotonicity constraints.',
  booktitle = 'Twenty First International Conference on Logic Programming',
  volume    = '3668',
  series    = 'Lecture Notes in Computer Science',
  publisher = 'Springer-Verlag',
  pages     = '326-340',
  year      = 2005,
  month     = 'October',
  available = ['ps']  
]).

bibentry(inproceedings,'esop2006',
[ author    = [codish,lagoon,'Peter Schachte',pjs],
  title     = 'Size-Change Termination Analysis in k-Bits',

  abstract = 'Size-change termination analysis is a simple and
    powerful technique successfully applied for a variety of programming
    paradigms. A main advantage is that termination for size-change
    graphs is decidable and based on simple linear ranking functions. A
    main disadvantage is that the size-change termination problem is
    PSPACE-complete. Proving size change termination may have to consider
    exponentially many size change graphs.   This paper is concerned
    with the representation of large sets of size-change graphs. The
    approach is constraint based and the novelty is that sets of
    size-change graphs are represented as disjunctions of size-change
    constraints.  A constraint solver to facilitate size-change
    termination analysis is obtained by interpreting size-change
    constraints over a sufficiently large but finite non-negative integer
    domain.  A Boolean k-bit modeling of size change graphs using
    binary decision diagrams leads to a concise representation.  
    Experimental evaluation indicates that the 2-bit representation
    facilitates an efficient implementation which is guaranteed complete
    for our entire benchmark suite.',
  booktitle = '15th European Symposium on Programming Languages 
               and Systems, ESOP 2006',
  volume    = '3924',
  series    = 'Lecture Notes in Computer Science',
  publisher = 'Springer-Verlag',
  pages     = '230-245',
  year      = 2006,
  month     = 'March',
  related   = [(source('talk_esop06.pdf'), 'slides from the talk')],   
  available = ['ps']  
]).


bibentry(inproceedings,'rta2006',
[ author    = [codish,lagoon,pjs],
  title     = 'Solving Partial Order Constraints for LPO Termination',

  abstract = 'This paper introduces a new kind of propositional encoding
    for reasoning about partial orders. The symbols in an unspecified
    partial order are viewed as variables which take integer values and
    are interpreted as indices in the order.
    For a partial order statement on n symbols each index is
    represented in ceiling(log_2 n) propositional variables and
    partial order constraints between symbols are modeled on the bit
    representations.
    We illustrate the application of our approach to determine LPO
    termination for term rewrite systems. Experimental results are
    unequivocal, indicating orders of magnitude speedups in comparison
    with current implementations for LPO termination.
    The proposed encoding is general and relevant to other applications
    which involve propositional reasoning about partial orders.',
  booktitle = 'International Conference on
               Rewriting Techniques and Applications, RTA 2006',
  volume    = '3924',
  series    = 'Lecture Notes in Computer Science',
  publisher = 'Springer-Verlag',
  pages     = '230-245',
  year      = 2006,
  month     = 'August',
  available = ['ps']  
]).

bibentry(inproceedings,'dppSat',
[ author = [codish,psk,lagoon, 'Ren&eacute; Thiemann','J&uuml;rgen Giesl'],
  title  = 'SAT Solving for Argument Filterings',
  abstract = 'This paper introduces a propositional encoding for lexicographic
  path orders in connection with dependency pairs. This facilitates
  the application of SAT solvers for termination analysis of term
  rewrite systems based on the dependency pair method. We address two
  main inter-related issues and encode them as satisfiability problems
  of propositional formulas that can be efficiently handled by SAT
  solving: (1) the combined search for a lexicographic path order
  together with an argument filtering to orient a set of
  inequalities; and (2) how the choice of the argument filtering
  influences the set of inequalities that have to be oriented.  We
  have implemented our contributions in the termination prover
  AProVE.  Extensive experiments show that by our encoding and the
  application of SAT solvers one obtains speedups in orders of
  magnitude as well as increased termination proving power.',
    booktitle = 'International Conference on
               Logic for Programming, Artificial Intelligence and Reasoning',
  volume    = 4246,
  series    = 'Lecture Notes in Artifical Intelligence',
  publisher = 'Springer-Verlag',
  pages     = '30-44',
  year      = 2006,
  month     = 'November',
  available = ['pdf']  
]).

bibentry(inproceedings,'rpoSat',
[ author = ['Elena Annov', codish,'J&uuml;rgen Giesl', 
            psk, 'Ren&eacute; Thiemann'],
  title  = 'A SAT-based Implementation  for RPO Termination',
  abstract = '    This paper introduces a propositional
    encoding of the recursive path order (RPO) on terms which is a
    combination of a multiset path order and a lexicographic path
    order which considers permutations of the arguments in the
    lexicographic comparison.
    The proposed encoding allows us to use SAT solvers in order to
    determine whether a given term rewrite system is RPO terminating.',
    booktitle = 'International Conference on
               Logic for Programming, Artificial Intelligence and Reasoning (Short Paper)',
  year      = 2006,
  month     = 'November',
  available = ['pdf']  
]).

bibentry(inproceedings,'rpoSatFrocos',
[ author = [psk, 'Ren&eacute; Thiemann','Elena Annov', codish,'J&uuml;rgen Giesl'],
  title  = 'Proving Termination using Recursive Path Orders
             and SAT Solving',
  abstract = 'We introduce a propositional encoding of the recursive
    path order with status (RPO). RPO is a combination of a multiset
    path order and a lexicographic path order which considers
    permutations of the arguments in the lexicographic comparison.
    Our encoding allows us to apply SAT solvers in order to
    determine whether a given term rewrite system is RPO-terminating.
    Furthermore, to apply RPO within the
    dependency pair framework, we combined our novel encoding for
    RPO with an existing encoding for argument filters.
    We implemented our contributions in the termination prover  AProVE.
    Our experiments show that due to our encoding, combining termination
    provers with SAT solvers improves the performance of RPO-implementations
    by orders of magnitude.',
    booktitle = 'FroCoS 2007 - 6th International Symposium on Frontiers of Combining Systems',
  year      = 2007,
  month     = 'September (to appear)',
  available = ['pdf']  
]).


bibentry(inproceedings,'cp07',
[ author = ['Olga Ohrimenko', pjs, codish],
  title  = 'Propagation = Lazy Clause Generation',

  abstract = 'Finite domain propagation solvers effectively represent
    the possible values of variables by a set of choices which can be
    naturally modelled as Boolean variables.  In this paper we describe
    how we can mimic a finite domain propagation engine, by mapping
    propagators into clauses in a SAT solver.  This immediately results in
    strong nogoods for finite domain propagation.  But a naive static
    translation is impractical except in limited cases.  We show how we
    can convert propagators to lazy clause generators for a SAT solver.
    The resulting system can solve scheduling problems significantly
    faster than generating the clauses from scratch, or using
    Satisfiability Modulo Theories solvers with difference logic.',
  booktitle = 'Proceedings of the 13th International Conference on 
          Principles and Practice of Constraint Programming,', 
  editor    = 'C. Bessiere',
  series    = 'LNCS',  
  volume    = 4741,    
  year      = 2007,
  pages     = '544-558',
  available = ['pdf']  
]).

bibentry(inproceedings,'lopstr07',
[ author = [codish],
  title  = 'Proving Termination with (Boolean) Satisfaction',
  abstract = 'At some point there was the Davis-Putnam-Logemann-Loveland (DPLL)
algorithm~\cite{DPLL62}.  Forty five years later, research on Boolean
satisfiability (SAT) is still ceaselessly generating even better SAT
solvers capable of handling even larger SAT instances. Remarkably, the
majority of these tools still bear the hallmark of the DPLL algorithm.
%
In sync with the availability of progressively stronger SAT solvers is
an accumulating number of applications which demonstrate that real
world problems can often be solved by encoding them into SAT. When
successful, this circumvents the need to redevelop complex search
algorithms from scratch. 

This presentation is about the application of Boolean SAT solvers to
the problem of determining program termination. Proving termination is
all about the search for suitable ranking functions. The key idea in
this work is to encode the search for particular forms of ranking
functions to Boolean statements which are satisfiable if and only if
such ranking functions exist. In this way, proving termination can be
performed using a state-of-the-art Boolean satisfaction solver.',
  booktitle    = 'The 17th International Symposium on Logic-Based 
Program Synthesis and Transformation (LOPSTR 2007)',      
  series    = 'LNCS',  
  volume    = 4915,    
  editor    = 'A. King',
  year      = 2008,
  pages     = '1-7',  
  related   = [(source('lopstr_slides07.pdf'), 'slides from the talk')],   
  available = ['pdf']  
]).


bibentry(inproceedings,'scnp07', %% TACAS08
[ author = ['Amir Ben-Amram',codish],
  title  = 'A SAT-Based Approach to Size Change Termination 
         with Global Ranking Functions',
  abstract = ' We describe a new approach to proving termination 
  with size change
  graphs.  This is the first decision procedure for size change
  termination (SCT) which makes direct use of global ranking
  functions.  It handles a well-defined and significant subset of SCT
  instances, designed to be amenable to a SAT-based solution.  We have
  implemented the approach using a state-of-the-art Boolean
  satisfaction solver.  Experimentation indicates that the approach is
  a viable alternative to the complete SCT decision procedure based on
  closure computation and local ranking functions.  Our approach has
  the extra benefit of producing an explicit witness to prove
  termination in the form of a global ranking function.',
  booktitle = 'Fourteenth International Conference on
        Tools and Algorithms for the Construction
        and Analysis of Systems (TACAS)',
  editor    = 'C. R. Ramakrishnan and Jakob Rehof',
  series    = 'LNCS',  
  volume    = ?,    
  pages     = 'To Appear',
  year      = 2008,     
  month     = 'March',
  related =      [(off_home('sct'), 'Online Analyzer')],
  available = ['pdf']
]).


bibentry(inproceedings,'AACGP08', %% 
[ author = ['Elvira Albert',  'Puri Arenas', codish,  genaim, 'German Puebla', 'Damiano Zanardini'],
  title  = 'Termination Analysis of Java Bytecode',
  abstract = 'Termination analysis has received considerable attention,
    traditionally in the context of declarative programming, and recently
    also for imperative languages. In existing approaches, termination is
    performed on source programs. However, there are many situations,
    including mobile code, where only the compiled code is available. In
    this work we present an automatic termination analysis for sequential
    Java Byte- code programs. Such analysis presents all of the challenges
    of analyzing a low-level language as well as those introduced by
    object-oriented languages. Interestingly, given a bytecode program, we
    produce a constraint logic program, CLP, whose termination entails
    termination of the byte- code program. This allows applying the large
    body of work in termination of CLP programs to termination of Java
    bytecode. A prototype analyzer is described and initial
    experimentation is reported.  ',
  booktitle = 'Formal Methods for Open Object-Based Distributed Systems,
               10th IFIP WG 6.1 International Conference, FMOODS 2008,
               Oslo, Norway, June 4-6, 2008, Proceedings',
  editor    = 'Gilles Barthe and Frank S. de Boer',
  series    = 'LNCS',  
  volume    = 5051,    
  pages     = '2-18',
  year      = 2008,     
  month     = ' ',
  available = ['pdf']
]).


bibentry(inproceedings,'iclp08',
[ author = [codish,lagoon,pjs],
  title  = 'Telecommunications Feature Subscription as a 
       Partial Order Constraint Problem',

  abstract = 'This paper describes the application of a partial order constraint
    solver to a telecommunications feature subscription configuration
    problem. 
    Partial order constraints are encoded to propositional logic and
    solved using a state-of-the-art Boolean satisfaction solver.
    The encoding is based on a symbol-based approach: symbols are
    viewed as variables which take integer values and are interpreted
    as indices in the order.
    Experimental evaluation indicates that partial order constraints
    are a viable alternative to previous solutions which apply
    constraint programming techniques and integer linear programming.',
  booktitle = 'Twenty Fourth International Conference on Logic Programming',
  editor    = 'Maria Garcia de la Banda and Enrico Pontelli',
  series    = 'LNCS',  
  volume    = ' ',    
  pages     = 'to appear',
  year      = 2008,     
  month     = 'August',
  available = ['pdf'],
  related =      [(off_home('Papers/Sources/iclp08data.pl'), 'random data instances'),
                  (off_home('Papers/Sources/cp08data.pl'), 'random data instances from CP08 paper'),
                  (source('feature_subscription.pdf'), 'a version with additional experiments')]
]).


bibentry(inproceedings,'ppdp09',
[ author = [codish,genaim,pjs],
  title  = 'A Declarative Encoding of Telecommunications 
       Feature Subscription in SAT',

  abstract = 'This paper describes the encoding of a telecommunications feature
  subscription configuration problem to propositional logic and its
  solution using a state-of-the-art Boolean satisfaction solver.
  The transformation of a problem instance to a corresponding
  propositional formula in conjunctive normal form is obtained in a
  declarative style. 
  An experimental evaluation indicates that our encoding is
  considerably faster than previous approaches based on the use of
  Boolean satisfaction solvers.
  The key to obtaining such a fast solver is the careful design of the
  Boolean representation and of the basic operations in the encoding.
  The choice of a declarative programming style makes the use of
  complex circuit designs relatively easy to incorporate into the
  encoder and to fine tune the application.',
  booktitle = 'Proceedings of the 11th International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming (PPDP 2009)',
  editor    = 'Ant{\'o}nio Porto and
               Francisco Javier L{\'o}pez-Fraguas',
  publisher = 'ACM Press',  
  pages     = '255--266',
  year      = 2009,     
  month     = 'September',
  available = ['pdf'],
  related =      [(off_home('Papers/Sources/cp08data.pl'), 'random data instances from CP08 paper')]
]).

bibentry(inproceedings,'lpar16',
[ author    = [codish,'Moshe Zazon-Ivry'],   
  title     = 'Pairwise Cardinality Networks',  
  abstract  = 'We introduce pairwise cardinality networks, 
  networks of comparators,
  derived from pairwise sorting networks, which express cardinality
  constraints. 
  We show that pairwise cardinality networks are superior to the
  cardinality networks introduced in previous work which are derived
  from odd-even sorting networks.
  Our presentation identifies the precise relationship between odd-even
  and pairwise sorting networks. This relationship also clarifies why 
  pairwise sorting networks have significantly better propagation
  properties for the application of cardinality constraints.', 
  booktitle = 'Proceedings of LPAR-16',       
  volume    = '?',       
  series    = 'LNAI',      
  publisher = 'springer',   
  pages     = '?',       
  year      = 2010,
  month     = '?',       
  available = ['pdf'],  
  related   =  [(off_home('Papers/Sources/lpar16.ppsx'), 'Slides')]
]).

bibentry(inproceedings,'lpar17',
[ author    = [codish,'Carsten Fuhs','J&uuml;rgen Giesl','Peter Schneider-Kamp'],   
  title     = 'Lazy Abstraction for Size-Change Termination',  
  abstract  = 'Size-change termination is a widely used means of proving termination
    where source programs are first abstracted to size-change graphs which
    are then analyzed to determine if they satisfy the size-change
    termination property.
    Here, the choice of the abstraction is crucial
    to the success of the method, and it is an open problem how to choose
    an abstraction such that no critical loss of precision occurs.
    %
    This paper shows how to couple the search for a suitable abstraction
    and the test for size-change termination via an encoding to a single
    SAT instance.  In this way, the problem of choosing the right
    abstraction is solved en passant by a SAT solver.
    %
    We show that for the setting of term rewriting, the integration of
    this approach into the dependency pair framework works smoothly
    and gives rise to a new class of size-change reduction pairs.
    We implemented size-change reduction
    pairs in the termination prover AProVE and evaluated their
    usefulness in extensive experiments.', 
  booktitle = 'Proceedings of LPAR-17',       
  volume    = '6397',       
  series    = 'LNCS',      
  publisher = 'springer',   
  pages     = '217-232',       
  year      = 2010,
  month     = 'October',       
  available = ['pdf']
]).

bibentry(inproceedings,'optimal_base_problem',
[ author = [codish,'Yoav Fekete',fuhs,psk],
  title  = 'Optimal Base Encodings for 
            Pseudo-Boolean Constraints',

  abstract = 'This paper formalizes the "optimal base problem", presents an
  algorithm to solve it, and describes its application to the encoding
  of Pseudo-Boolean constraints to SAT.  We demonstrate the impact of
  integrating our algorithm within the Pseudo-Boolean constraint
  solver MiniSAT+.  Experimentation indicates that our algorithm
  scales to consider bases involving numbers up to 1,000,000,
  improving on the restriction in MiniSAT+ to prime numbers up to
  17.  We show that, while for many examples primes up to 17 do
  suffice, encoding with respect to arbitrary bases improves the
  subsequent SAT solving time considerably.',

  booktitle = 'Proceedings of TACAS 2011',   
  institution = 'Department of Computer Science; 
                 Ben-Gurion University',
  year      = 2011,     
  month     = 'March',
  related =  [(url('http://arxiv.org/abs/1007.4935'),
            'e-print from arXiv.org'),
             (url('http://aprove.informatik.rwth-aachen.de/forms/unified_form_PBB.asp'),
            'online optimal base finder')],
  available = []
]).

bibentry(inproceedings,'equi',
[ author = ['Amit Metodi', codish, lagoon, pjs],
  title  = 'Equi-propagation for Optimized SAT Encoding',

  abstract = 'We present an approach to propagation based SAT
  encoding, Boolean equi-propagation, where constraints are modelled
  as Boolean functions which propagate information about equalities
  between Boolean literals.  This information is then applied as a
  form of partial evaluation to simplify constraints prior to their
  encoding as CNF formulae.  We demonstrate for a variety of
  benchmarks that our approach leads to a considerabe reduction in the
  size of CNF encodings and subsequent speed-ups in SAT solving
  times.',

  booktitle = 'Proceedings of CP 2011',   
  year      = 2011,     
  month     = 'September',
  related   = [(url('http://arxiv.org/abs/1104.4617'),
            'available on arxiv')],
  available = []
]).



bibentry(inproceedings,'aaai-2012',
[ author = ['Amit Metodi', 'Roni Stern', 'Meir Kalech', codish],
  title  = 'Compiling Model-Based Diagnosis to Boolean Satisfaction',
  abstract = 'This paper introduces an encoding of Model Based
  Diagnosis (MBD) to Boolean Satisfaction (SAT) focusing on minimal
  cardinality diagnosis.  The encoding is based on a combination of
  sophisticated MBD preprocessing algorithms and SAT compilation
  techniques which together provide concise CNF formula.  Experimental
  evidence indicates that our approach is superior to all published
  algorithms for minimal cardinality MBD.  In particular, we can
  determine, for the first time, minimal cardinality diagnoses for the
  entire standard ISCAS-85 benchmark.  Our results open the
  way to improve the state-of-the-art on a range of similar MBD
  problems.',

  booktitle = 'Proceedings of AAAI 2012',   
  year      = 2012,     
  month     = 'July',
  related   =  [
          (url('http://amit.metodi.me/research/scrypto/'),
                       'The SCryptoMiniSAT wrapper,'),
          (url('http://amit.metodi.me/research/mbdsolver/'),
                       'The SAT based MBD diagnoser (for Windows),'),
          (url('http://amit.metodi.me/research/mbdsolver/paperExprsCSVs.zip'),
                       'More details on the AAAI benchmarks')
               ],
  available = ['pdf']
]).

bibentry(inproceedings, ijcai2013,
[ author    = [codish,'Alice Miller','Patrick Prosser',pjs],   
  title     = 'Breaking Symmetries in Graph Representation',       
  abstract  = 'There are many complex combinatorial problems which involve
  searching for an undirected graph satisfying a certain
  property. These problems are often highly challenging because of the
  large number of isomorphic representations of a possible solution.
  In this paper we introduce novel, effective and compact, symmetry
  breaking constraints for undirected graph search.  While incomplete,
  these prove highly beneficial in pruning the search for a graph.  We
  illustrate the application of symmetry breaking in graph
  representation to resolve several open instances in extremal graph
  theory.', 
  booktitle = 'IJCAI 2013, Proceedings of the 23rd International Joint
               Conference on Artificial Intelligence',       
  volume    = '',       
  series    = '',      
  publisher = 'IJCAI/AAAI',   
  pages     = '',       
  year      = 2013,
  month     = 'August',  
  related   = [(url('http://ijcai.org/papers13/Papers/IJCAI13-083.pdf'),
            'Online Proceedings')],
  available = ['pdf']
]).

bibentry(inproceedings,'cep2013',
[ author    = [codish,  'Yoav Fekete',  'Amit Metodi'],
  title     = 'Backbones for Equality',       
  abstract  = '
  This paper generalizes the notion of the backbone of a CNF formula
  to capture also equations between literals. Each such equation
  applies to remove a variable from the original formula thus
  simplifying the formula without changing its satisfiability, or the
  number of its satisfying assignments.
  We prove that for a formula with n variables, the generalized
  backbone is computed with at most n+1 satisfiable calls and exactly
  one unsatisfiable call to the SAT solver.
  We illustrate the integration of generalized backbone computation to
  facilitate the encoding of finite domain constraints to SAT. In this
  context generalized backbones are computed for small groups of
  constraints and then propagated to simplify the entire constraint
  model.
  A preliminary experimental evaluation is provided.
', 
  booktitle = 'Proceedings of the Ninth Haifa Verification Conference',       
  volume    = '',       
  series    = 'LNCS',      
  publisher = '',   
  pages     = '',       
  year      = 2013,
  month     = 'November',       
  available = [pdf]
]).

bibentry(inproceedings,'rns2014',
[ author    = ['Yoav Fekete',  codish],
  title     = 'Simplifying Pseudo-Boolean Constraints in Residual Number
  Systems',       
  abstract  = '
  We present an encoding of pseudo-Boolean constraints based on
  decomposition with respect to a residual number system.  We
  illustrate that careful selection of the base for the residual
  number system, and when bit-blasting modulo arithmetic, results in a
  powerful approach when solving hard pseudo-Boolean constraints.  We
  demonstrate, using a range of pseudo-Boolean constraint solvers,
  that the obtained constraints are often substantially easier to
  solve.
', 
  booktitle = '17th International Conference on Theory and Applications of 
               Satisfiability Testing (SAT 2014)',       
  volume    = '',       
  series    = 'LNCS',      
  publisher = '',   
  pages     = '',       
  year      = 2014,
  month     = 'July',       
  available = [pdf]
]).


bibentry(inproceedings,'lata2015',
[ author    = [codish,'Luis Cruz-Filipe',psk],
  title     = 'Sorting Networks: The End Game',       
  abstract  = '
  This paper studies properties of the back end of a sorting network
  and illustrates the utility of these in the search for networks of
  optimal size or depth. All previous works focus on properties of the
  front end of networks and on how to apply these to break symmetries
  in the search. The new properties help shed understanding on how
  sorting networks sort and speed-up solvers for both optimal size and
  depth by an order of magnitude.
', 
  booktitle = 'Language and Automata Theory and Applications - 9th International
               Conference, {LATA}',       
  volume    = '8977',       
  series    = 'LNCS',      
  publisher = 'Springer',   
  pages     = '664--675',       
  year      = 2015,
  month     = 'March',       
  available = []
]).


bibentry(inproceedings,'lopstr2015',
[ author    = [codish,'Luis Cruz-Filipe','Markus Nebe',psk],
  title     = 'Applying Sorting Networks to Synthesize Optimized Sorting Libraries',       
  abstract  = '
  This paper shows an application of the theory of sorting networks to
  facilitate the synthesis of optimized general purpose sorting
  libraries. Standard sorting libraries are often based on
  combinations of the classic Quicksort algorithm with insertion sort
  applied as the base case for small fixed numbers of
  inputs. Unrolling the code for the base case by ignoring loop
  conditions eliminates branching and results in code which is
  equivalent to a sorting network. This enables the application of
  further program transformations based on sorting network
  optimizations, and eventually the synthesis of code from sorting
  networks.
  We show that if considering the number of comparisons and swaps
  then theory predicts no real advantage of this
  approach. However, significant speed-ups are obtained when taking
  advantage of instruction level parallelism and non-branching
  conditional assignment instructions, both of which are common in
  modern CPU architectures.
  We provide empirical evidence that using code synthesized from
  efficient sorting networks as the base case for Quicksort libraries
  results in significant real-world speed-ups.

', 
  booktitle = 'Logic-Based Program Synthesis and Transformation (LOPSTR), Revised Selected Papers',       
  volume    = '9527',       
  series    = 'LNCS',      
  publisher = 'Springer',   
  pages     = '127--142',       
  year      = 2015,     
  available = []
]).

/*

*/


%%% UNPUBLISHED TECH_REPORTS

bibentry(tech_report,'optimal_base_problem',
[ author = [codish,'Yoav Fekete',fuhs,psk],
  title  = 'Optimal Base Encodings for 
            Pseudo-Boolean Constraints',

  abstract = 'This paper formalizes the "optimal base problem", presents an
  algorithm to solve it, and describes its application to the encoding
  of Pseudo-Boolean constraints to SAT.  We demonstrate the impact of
  integrating our algorithm within the Pseudo-Boolean constraint
  solver MiniSAT+.  Experimentation indicates that our algorithm
  scales to consider bases involving numbers up to 1,000,000,
  improving on the restriction in MiniSAT+ to prime numbers up to
  17.  We show that, while for many examples primes up to 17 do
  suffice, encoding with respect to arbitrary bases improves the
  subsequent SAT solving time considerably.',


  institution = 'Department of Computer Science; 
                 Ben-Gurion University',
  year      = 2010,     
  month     = 'May',
  related =  [(url('http://arxiv.org/abs/1007.4935'),
            'e-print from arXiv.org'),
             (url('http://aprove.informatik.rwth-aachen.de/forms/unified_form_PBB.asp'),
            'online optimal base finder')],
  available = []
]).

bibentry(tech_report,'sortingNetworks2014',
[ author = [codish,'Luis Cruz-Filipe',psk],
  title  = 'The Quest for Optimal Sorting Networks: Efficient Generation of
       Two-Layer Prefixes',

  abstract = '
  Previous work identifying depth-optimal $n$-channel sorting networks
  for 9 leq n leq 16 is based on exploiting symmetries of the first
  two layers.  However, the naive generate-and-test approach typically
  applied does not scale.
  This paper revisits the problem of generating two-layer prefixes
  modulo symmetries. An improved notion of symmetry is provided and a
  novel technique based on regular languages and graph isomorphism is
  shown to generate the set of non-symmetric representations.  An
  empirical evaluation demonstrates that the new method outperforms
  the generate-and-test approach by orders of magnitude and easily scales 
  until $n=40$.
  ',
  institution = 'International Symposium on Symbolic and 
                 Numeric Algorithms for Scientific Computing (Timisoara, Romania)',
  year      = 2014,     
  month     = 'September',
  related =  [(url('http://arxiv.org/abs/1404.0948'),
            'e-print from arXiv.org')],
  available = []
]).


bibentry(tech_report,'sortingNetworksSize2014',
[ author = [codish,'Luis Cruz-Filipe','Michael Frank',psk],
  title  = 'Twenty-Five Comparators is Optimal when Sorting Nine Inputs
  (and Twenty-Nine for Ten)',

  abstract = '
  This paper describes a computer-assisted non-existence proof of
  9-input sorting networks consisting of 24 comparators, hence
  showing that the 25-comparator sorting network found by Floyd in
  1964 is optimal. As a corollary, we obtain that the 29-comparator
  network found by Waksman in 1969 is optimal when sorting 10 inputs.
%
  This closes the two smallest open instances of the optimal-size sorting
  network problem, which have been open since the results of Floyd and
  Knuth from 1966 proving optimality for sorting networks of
  up to 8 inputs.
%
  The proof involves a combination of two methodologies: one based on
  exploiting the abundance of symmetries in sorting networks, and the
  other based on an encoding of the problem to that of satisfiability
  of propositional logic. We illustrate that, while each of these can
  single-handedly solve smaller instances of the problem, it is their
  combination that leads to the more efficient solution that scales to
  handle 9 inputs.
  ',


  institution = 'IEEE International Conference on Tools with Artificial Intelligence (ICTAI) ',
  year      = 2014,     
  month     = 'November',
  related =  [(url('http://arxiv.org/abs/1405.5754'),
            'e-print from arXiv.org')],
  available = []
]).





bibentry(tech_report,'ramsey2014',
[ author = [codish,'Michael Frank','Avraham Itzhakov','Alice Miller'],
  title  = 'Solving Graph Coloring Problems with Abstraction and\\ Symmetry:
  the Ramsey Number $R(4,3,3)=30$',

  abstract = '
    This paper introduces a methodology that can be applied to solve graph
  edge-coloring problems and in particular has been used to prove that the Ramsey
  number $R(4,3,3)=30$.
%
  The number $R(4,3,3)$ is often presented as the unknown Ramsey
  number with the best chances of being found ``soon''. Yet, it has
  remained an open problem for more than 50 years.
%
  The proposed technique is based on two well-studied concepts,
  \emph{abstraction} and \emph{symmetry}. First, we introduce an
  abstraction on graph colorings, \emph{degree matrices}, that specify
  the degree of each vertex in each color. We compute, using a SAT
  solver, an over-approximation of the set of degree matrices of all
  solutions of the graph coloring problem.
%
  Then, for each degree matrix in the over-approximation, we compute,
  again using a SAT solver, the set of all solutions with matching
  degrees.
%
  Breaking symmetries, on degree matrices in the first step and with
  respect to graph isomorphism in the second, is cardinal to the
  success of the approach.
%
  We illustrate the approach via two applications: proving that $R(4,3,3)=30$ and 
  computing the  previously unknown number  of $(3,3,3;13)$
  Ramsey colorings (78{,}892).
  ',


  institution = 'Ben-Gurion University of the Negev',
  year      = 2014,     
  month     = 'September',
  related =  [(url('http://arxiv.org/abs/1409.5189'),
            'e-print from arXiv.org')],
  available = []
]).






/*
bibentry(tech_report,'meta_circ',
[ author = [codish,harald],
  title  = 'Meta-Circular Abstract Interpretation in Prolog',

  abstract = 'We give an introduction to the meta-circular approach to
     the abstract interpretation of logic programs.  This approach is
     particularly useful for prototyping and for introductory classes
     on abstract interpretation.  Using interpreters, students can
     immediately write, adapt, and experiment with interpreters and
     working dataflow analysers.  We use a simple meta-circular
     interpreter, based on a "non-ground Tp" semantics, as a
     generic analysis engine.  Instantiating the engine is a matter of
     providing an appropriate domain of approximations, together with
     definitions of "abstract" unification and disjunction.  Small
     changes of the interpreter let us vary both what can be
     "observed" by an analyser, and how fixed point computation is
     done.  Amongst the dataflow analyses used to exemplify this
     approach are a parity analysis, groundness dependency analysis,
     call patterns, depth-k analysis, and a "pattern" analysis to
     establish most specific generalisations of calls and success
     sets.',


  institution = 'Department of Computer Science; 
                 Ben-Gurion University',
  year      = 2001,     
  month     = 'June',
  related =      [(off_home('Tutorial'), 'Companion Web Site')],
  available = ['ps.gz']
]).
*/
