title: Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

authors:
Wei-Jia Huang
Christophe Chareton
Yu-Fang Chen
Kai-Min Chung
Min-Hsiu Hsieh
Alfons Laarman
Jingyi Mei

abstract: Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.


venue: tacas

title: Multiple Long-Run and ømega-Regular Objectives in MDPs

authors:
Julius Ide
Joost-Pieter Katoen
Hannah Mertens
Tim Quatmann

abstract: We consider Markov decision processes (MDPs) with three types of objectives: (1) the probability of satisfying an $$\omega $$ -regular objective, (2) the expected long-run average (LRA) reward, and (3) the probability that the long-run average reward exceeds a given threshold. All types of objectives address infinite system behavior. The challenge lies in capturing all possible trade-offs between satisfiable LTL formulas and achievable LRA rewards inside the end components (ECs) of the MDP. Our approach translates LTL to Rabin objectives and then splits ECs into various sub-components in which (a subset of) the Rabin objectives are satisfied. LRA expectation and threshold satisfaction objectives are then optimized in those sub-components independently, where we exploit iterative techniques for multiple expected LRA reward objectives. We realized the approach into the Storm model checker and empirically show feasibility of verification of large models with more than half a million states—outperforming a reference implementation based on linear programming by several orders of magnitude.


title: Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees

authors:
Nat Karmios
Sacha-Élie Ayoun
Philippa Gardner


title: Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities

authors:
Ali Rasim Kocal
Michael Schwarz
Simmo Saan
Helmut Seidl


title: Parallel SMT Solving via Iterative Tree Partitioning

authors:
Tomás Kolárik
Antti E. J. Hyvärinen
Seyedmasoud Asadzadeh
Natasha Sharygina

abstract: We present a novel algorithm for parallel solving of SMT problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT . Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF_LRA and QF_LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.


title: Enumerating Choice Terms in Model-Based Quantifier Instantiation

authors:
Lydia Kondylidou
Andrew Reynolds
Jasmin Blanchette
Cesare Tinelli

abstract: Satisfiability modulo theories (SMT) solvers are widely used for determining the satisfiability of logical formulas with respect to background theories. SMT solvers are traditionally based on first-order logic, but some also support higher-order logic. Recently, Kondylidou et al. introduced model-based quantifier instantiation with fast enumeration (MBQI-Enum), a quantifier instantiation strategy that works for both logics. A weakness of MBQI-Enum is that it does not find refutations when Hilbert choice terms are necessary. In this work, we present an extension of MBQI-Enum that enables it to reason effectively about Hilbert’s choice operator. The extended strategy substantially increases the success rate of the SMT solver cvc5 on higher-order benchmarks.


title: Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination

authors:
Lukas König
Christian Schildwächter
Michaela Klauck
Christian Heinzemann


title: SMT(LIA) Sampling with High Diversity

authors:
Yong Lai
Junjie Li
Chuan Luo

abstract: SMT sampling refers to the task of generating a set of satisfying assignments (samples) for a given SMT formula. An effective SMT sampler should be capable of producing samples with high diversity to maximize coverage of the solution space. However, most SMT samplers struggle to adequately cover the solution space and fail to generate sufficiently diverse solutions. To address these limitations, we propose $$ HighDiv $$ , the first iterative sampling framework that integrates CDCL(T) and local search in a bidirectional guided manner. During the bidirectional guidance process, solutions generated by CDCL(T) guide the variable initialization of the local search. Conversely, solutions produced by the local search guide CDCL(T) to further explore the solution space. Additionally, we design a novel local search algorithm, Context-Constrained Stochastic Search (CCSS), which introduces the Constraint-Partitioned Variable Initialization and the boundary-aware move operator. These components effectively balance exploration and feasibility throughout the search process. We conduct an extensive evaluation on QF_LIA formulas from the SMT-LIB benchmark. The results demonstrate that $$ HighDiv $$ achieves substantial improvements in diversity over the state-of-the-art SMT sampling tools.


title: Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)

authors:
Kilian Lichtner
Pascal Bergsträßer
Moses Ganardi
Anthony W. Lin
Georg Zetzsche

abstract: Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques, which are not expressible in first-order logic. Among others, these include liveness verification and monadic decomposability. We present the tool REAL, which implements an efficient elimination of Ramsey quantifiers in existential linear arithmetic theories over integers (LIA), reals (LRA), and the mixed case (LIRA). The tool supports a convenient input format, which is an extension of SMT-LIB over the aforementioned theories with Ramsey quantifiers. We also demonstrate a substantial speedup from the original prototype. As an application, we provide an automatic translation from FASTer (a tool for verifying reachability over infinite-state systems) output format to our extension of SMT-LIB and show how our tool extends FASTer to liveness checking.


title: SWAT: Improvements to the Symbolic Executor (Competition Contribution)

authors:
Nils Loose
Florian Sieck
Felix Mächtle
Thomas Eisenbarth


title: Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

authors:
Raz Lotan
Neta Elad
Oded Padon
Sharon Shoham


title: Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

authors:
Chia-Hsuan Lu
Tony Tan
Michael Benedikt

abstract: Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, an important issue is the detection of attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the adversarial robustness problem – determining whether an attack exists – were originally developed for image classification. In the case of graph learning, the attack model usually considers changes to the graph structure in addition to or instead of the numerical features of the input, and the state of the art techniques proceed via reduction to constraint solving, working on top of powerful solvers, e.g. for mixed integer programming. We show that it is possible to improve on the state of the art in structural robustness by replacing the use of powerful solvers by calls to efficient partial solvers, which run in polynomial time but may be incomplete. We evaluate our tool $$\textsc {RobLight} $$ on a diverse set of GNN variants and datasets.


title: Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis

authors:
Chien-Kai Ma
Bo-Hung Chen
Tian-Fu Chen
Dah-Wei Chiou
Jie-Hong R. Jiang

abstract: We develop error-tolerant quantum state discrimination(QSD) strategies that maintain reliable performance under moderate noise. Two complementary approaches are proposed: CrossQSD, which generalizes unambiguous discrimination with tunable confidence bounds to balance accuracy and efficiency, and FitQSD, which optimizes the measurement outcome distribution to approximate that of the ideal noiseless case. Furthermore, we provide a unified hybrid-objective QSD framework that continuously interpolates between minimum-error discrimination (MED) and FitQSD, allowing flexible trade-offs among competing objectives. The associated optimization problems are formulated as convex programs and efficiently solved via disciplined convex programming or, in many cases, semidefinite programming. Additionally, a circuit synthesis framework based on a modified Naimark dilation and isometry synthesis enables hardware-efficient implementations with substantially reduced qubit and gate resources. An open-source toolkit automates the full optimization and synthesis workflow, providing a practical route to QSD on current quantum devices.


title: DASA: Fully Gradient-Based Program Analysis (Competition Contribution)

authors:
Felix Mächtle
Jan-Niclas Serr
Nils Loose
Thomas Eisenbarth


title: Faster Signature Refinement for Branching Bisimilarity Minimization

authors:
Jan Martens
Maurice Laveaux

abstract: We present a new algorithm to efficiently minimize state spaces with respect to branching bisimilarity. Our approach combines signature-based refinement with Hopcroft’s “process-the-smaller-half” optimization to avoid unnecessary computation. This combination results in a conceptually simpler and empirically faster algorithm for state space minimization modulo branching bisimilarity. While the theoretical worst-case complexity is slightly worse than existing algorithms, empirical evaluations on benchmarks demonstrate significantly better performance.


title: Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution)

authors:
Marco Milanese
Raphaël Monat
Abdelraouf Ouadjaout
Antoine Miné

abstract: . We present advances we brought to Mopsa for SV-COMP 2026. Mopsa now supports a backward analysis mode which computes an under-approximation of the weakest liberal precondition for the alarms found during a verification pass, which generates an input harness to re-produce the incorrectness condition. We also added support for termination checking through the introduction of loop counters. With these improvements, Mopsa wins the SoftwareSystems category, and ranks third in the TrueOverall category.


title: Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring

authors:
Mahrokh Mirani
Paola Inverardi
Patrizio Pelliccione
Franco Raimondi
Nicolas Troquard


title: Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP

authors:
Charles Moloney
Robert Dyer
Elena Sherman


title: EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution)

authors:
Milán Mondok
Csanád Telbisz
Levente Bajczi
Dániel Kovács
Mihály Dobos-Kovács
Vince Molnár


title: Deconstructing Subset Construction - Reducing While Determinizing

authors:
John Nicol
Markus Frohme


title: Bit-Precise Interpolation in Bitwuzla

authors:
Aina Niemetz
Mathias Preiner

abstract: Bitwuzla is a state-of-the-art SMT solver specialized in theories relevant to bit-precise reasoning. The main bit-vector solving procedure of Bitwuzla is based on bit-blasting, a reduction of bit-vector constraints to propositional logic (SAT). Until now, Bitwuzla did not support interpolant generation, which is a key requirement for many verification applications that rely on bit-precise reasoning. We present an extension of Bitwuzla with the capability to produce interpolants and interpolation sequences for quantifier-free bit-vector formulas. Our interpolation workflow extracts bit-level interpolants from proofs produced by the back-end SAT solver, which are lifted to the word-level and post-processed to recover and simplify word-level structure. We evaluate our new bit-vector interpolation engine in the context of various interpolation-based algorithms for symbolic model checking.


title: Efficient Verification of Lingua Franca Programs

authors:
Peter Csaba Ölveczky
Mario Reja
Mikheil Rukhaia
Kyungmin Bae
Mircea Marin


title: jMT: Testing Correctness of Java Memory Models

authors:
Lukas Panneke
Heike Wehrheim

abstract: Folklore is often saying"The Java memory model is broken."Therefore, several approaches have proposed repairs, only to find new programs exhibiting unexpected, unintuitive behavior or the model forbidding standard compiler optimizations. The complexity of defining a memory model for concurrent Java lies in the fact that it requires a multi-execution model. Multi-execution models need to inspect the many potential executions of a program in order to find the valid ones. Tools automatically validating novel proposals of Java memory models are, however, largely lacking. To alleviate this problem, we introduce jMT, a novel tool for constructing multi-execution semantics for concurrent Java programs. jMT relies on single-execution models defining well-formed execution graphs, based on which it builds valid multi-execution semantics via causality checking. Thereby, jMT supports evaluating new proposals of Java memory models (JMMs) on a per-program basis. jMT can furthermore be employed for testing the conformance of JMMs to existing compilation schemes and compilers. Our evaluation of jMT on 169 litmus tests reveals a number of interesting insights into existing JMMs.


title: Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml

authors:
João Madeira Pereira
Filipe Marques
Pedro Adão
Hichem Rami Ait El Hara
Léo Andrès
Arthur Carcano
Pierre Chambart
Petar Maksimovic
Nuno Santos
José Fragoso Santos

abstract: SMT solvers are essential for applications in artificial intelligence, software verification, and optimisation. However, no single solver excels across all formula types, and different applications may require the use of different solvers. While the SMT-LIB language enables multi-solver support, it also incurs heavy I/O overhead. To address this, we introduce Smt.ml , an SMT-solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability. Furthermore, Smt.ml is the only SMT frontend that includes a simplification-management engine for streamlining the integration of new formula simplifications and the verification of their correctness. Our evaluation demonstrates that Smt.ml ’s results are consistent with those of its backend solvers and that its optimisations are highly effective on formulas generated from the symbolic execution of an extensive program-analysis benchmark.


title: CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems

authors:
Roberto Pettinau
Christoph Matheja


title: QSOLE: Automatic QBF Equivalence Checking

authors:
Peter Pfeiffer
Mark Peyrer
Daniel Große
Martina Seidl

abstract: Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains such as formal verification, synthesis, and symbolic AI. Despite progress in solving techniques, less attention has been given to the infrastructure for constructing correct and efficient QBF encodings. For instance, it is often unclear whether two QBFs that encode the same problem in different ways yield the same solutions. Traditional QBF equivalence checking focuses only on free variables, yet in many cases, the quantified variables must also be considered. In this paper, we present QSOLE , the first fully automatic checker for solution-based QBF equivalence. Based on a recently introduced approach, QSOLE decomposes equivalence checks into smaller entailment computations and is capable of generating witnesses for detected inequivalences, which can be used to debug encodings. Furthermore, it allows for explicit exclusion of variables from equivalence checks enabling comparison of formulas using different local auxiliary variables.


title: DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling

authors:
Francesca Randone
Romina Doz
Mirco Tribastone
Luca Bortolussi

abstract: We present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and replaces measure-zero predicates and discrete branches with a vanishing smoothing, yielding closed-form expressions for posterior and path probabilities. We prove differentiability of these quantities with respect to program parameters, enabling end-to-end optimization via standard automatic differentiation, without Monte Carlo estimators. On thirteen benchmark programs, DeGAS achieves accuracy and runtime competitive with variational inference and MCMC. Importantly, it reliably tackles optimization problems where sampling-based baselines fail to converge due to conditioning involving continuous variables.


title: ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs - (Competition Contribution)

authors:
Naïm Moussaoui Remil
Caterina Urban


title: Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation - (Competition Contribution)

authors:
Simmo Saan
Ali Rasim Kocal
Michael Petter
Karoliine Holter
Julian Erhard
Michael Schwarz
Vesal Vojdani
Helmut Seidl


title: Trace Repair for Temporal Behavior Trees

authors:
Sebastian Schirmer
Philipp Schitz
Johann C. Dauer
Bernd Finkbeiner
Sriram Sankaranarayanan

abstract: We present methods for repairing traces against specifications given as temporal behavior trees (TBT). TBT are a specification formalism for action sequences in robotics and cyber-physical systems, where specifications of sub-behaviors, given in signal temporal logic, are composed using operators for sequential and parallel composition, fallbacks, and repetition. Trace repairs are useful to explain failures and as training examples that avoid the observed problems. In principle, repairs can be obtained via mixed-integer linear programming (MILP), but this is far too expensive for practical applications. We present two practical repair strategies: (1) incremental repair, which reduces the MILP by splitting the trace into segments, and (2) landmark-based repair, which solves the repair problem iteratively using TBT’s robust semantics as a heuristic that approximates MILP with more efficient linear programming. In our experiments, we were able to repair traces with more than 25 000 entries in under ten minutes, while MILP runs out of memory.


title: Real-time Proof Checking for Distributed Incremental SAT Solving

authors:
Dominik Schreiber
Mathias Fleury
Katalin Fazekas
Armin Biere

abstract: Distributed clause-sharing SAT solvers are powerful automated reasoning tools capable of rapidly solving many difficult instances. Users of SAT solving often rely on incremental SAT solving, i.e., interactive solve calls over an evolving formula. We present the first approach to distributed incremental SAT solving that grants full confidence in the obtained result. Specifically, we extend a recent distributed real-time proof checking approach with an incremental proof interface. Our approach offers great flexibility in that it supports dynamic re-scheduling of computational resources and enables safely sharing clauses across tasks that operate on deviating assumptions and formula increments. We further add on-the-fly clause compression to checkers in order to reduce memory consumption. Experiments with the distributed solver MallobSat on up to 1216 cores show that our trusted solving approach checks incremental SAT tasks with small mean overhead ( $$< 33$$ %) over unchecked solving.


title: Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob

authors:
Dominik Schreiber
Aina Niemetz
Mathias Preiner

abstract: We present a distributed platform for massively parallel SMT solving that supports various theories for bit-precise reasoning, with and without quantifiers and push-pop incrementality. Our system is based on an integration of the state-of-the-art SMT solver Bitwuzla into the distributed job scheduling and automated reasoning platform Mallob, which allows Bitwuzla to make heavy use of Mallob ’s distributed incremental SAT solving engine. Our experimental evaluation shows that this approach outperforms prior SMT parallelization approaches and achieves unprecedented speedups at up to 768 cores.

awards:
Best Tool Paper
Distinguished Artifact
Distinguished Paper


title: Exploring the SMT-LIB Benchmark Library

authors:
Hans-Jörg Schurr
François Bobot
Mathias Preiner
Aina Niemetz
Clark W. Barrett
Pascal Fontaine
Cesare Tinelli

abstract: The SMT-LIB benchmark collection is a large set of problems for SMT solvers. It has been continuously maintained and expanded since its creation in the early 2000s by the SMT-LIB initiative. It has been used since 2005 by the annual SMT solver competition to compare the performance of SMT solvers, and by researchers to study novel solving techniques. Effective use of the collection often requires access to benchmark metadata (e.g., date, source, satisfiability status, theory symbol count, and so on). Furthermore, this metadata and the past competition results contain a wealth of historical information about the development of SMT solving. In this paper, we report on our efforts to collect and curate all metadata from the SMT-LIB benchmarks together with the results of all past SMT-COMP competitions in a single SQLite database. We also present tools to explore this database and extract relevant insights. Since APIs for SQLite databases are available for all major programming languages, the database makes it easy to add features using SMT benchmark metadata to SMT development tools. To illustrate the structure of the collected data we perform multiple case studies. In particular, we present a comparison of SMT solvers that is independent of the changing hardware and benchmarks used by the competition. The database is released annually on Zenodo, and serves as an archive of the state of SMT-LIB and, by extension, of the state of the art in SMT.


title: Re3ver: Reverse and Verify - (Competition Contribution)

authors:
Adéla Stepková
Martin Jonás
Jan Strejcek


title: VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

authors:
Chuyue Sun
Yican Sun
Daneshvar Amrollahi
Ethan Zhang
Shuvendu K. Lahiri
Shan Lu
David L. Dill
Clark W. Barrett


title: Data Structure Analysis for Binaries

authors:
Sadra Bayat Tork
Nicholas Coughlin
Alicia Michael
James Tobler
Kirsten Winter


title: Automatically Tightening Access Control Policies with Restricter

authors:
Ka Lok Wu
Christa Jenkins
Scott D. Stoller
Omar Chowdhury

abstract: Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging task even for experienced administrators. In this paper, we set out to address this pain point by proposing Restricter , which automatically tightens each (permit) policy rule of a policy with respect to an access log, which captures some already exercised access requests and their corresponding access decisions ( i.e. , allow or deny). Restricter achieves policy tightening by reducing the number of access requests permitted by a policy rule without sacrificing the functionality of the underlying system it is regulating. We implement Restricter for Amazon’s Cedar policy language and demonstrate its effectiveness through two realistic case studies.


title: Quantifier Elimination Meets Treewidth

authors:
Hao Wu
Jiyu Zhu
Amir Kafshdar Goharshady
Jie An
Bican Xia
Naijun Zhan

abstract: In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth , a parameter that measures the graph’s tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.


venue: toplas

title: A Space Efficient Dynamic Allocation Algorithm for Queuing Messages

authors:
Eric Beyer
Peter Buneman

abstract: A simple dynamic allocation algorithm is described for queuing variable length messages in memory. The algorithm makes use of the ability of many operating system to increase and decrease available memory as required. Some results describing its efficiency are presented.


title: Compact Encodings of List Structure

authors:
Daniel G. Bobrow
Douglas W. Clark

abstract: List structures provide a general mechanism for representing easily changed structured data, but can introduce inefficiencies in the use of space when fields of uniform size are used to contain pointers to data and to link the structure. Empirically determined regularity can be exploited to provide more space-efficient encodings without losing the flexibility inherent in list structures. The basic scheme is to provide compact pointer fields big enough to accommodate most values that occur in them and to provide “escape” mechanisms for exceptional cases. Several examples of encoding designs are presented and evaluated, including two designs currently used in Lisp machines. Alternative escape mechanisms are described, and various questions of cost and implementation are discussed. In order to extrapolate our results to larger systems than those measured, we propose a model for the generation of list pointers and we test the model against data from two programs. We show that according to our model, list structures with compact cdr fields will, as address space grows, continue to be compacted well with a fixed-width small field. Our conclusion is that with a microcodable processor, about a factor of two gain in space efficiency for list structure can be had for little or no cost in processing time.


title: A Hierarchial Approach to Formal Semantics With Application to the Definition of PL/CS

authors:
Robert L. Constable
James E. Donahue

abstract: We describe a means of presenting hierarchically organized formal definitions of programming languages using the denotational approach of D. Scott and C. Strachey. As an example of our approach, we give the semantics of PL/CS, an instructional variant of PL/I. We also discuss the implications of this approach to language design, pointing out some cases where the wrong choices may cause the hierarchy to collapse into chaotic rubble.


title: Programming by Refinement, as Exemplified by the SETL Representation Sublanguage

authors:
Robert B. K. Dewar
Arthur Grand
Ssu-Cheng Liu
Jacob T. Schwartz
Edmond Schonberg

abstract: “Pure” SETL is a language of very high level allowing algorithms to be programmed rapidly and succintly. SETL's representation sublanguage adds a system of declarations which allow the user of the language to control the data structures that will be used to implement an algorithm which has already been written in pure SETL, so as to improve its efficiency. Ideally no rewriting of the algorithm should be necessary. The facilities provided by the representation sublanguage and the run-time data structures that it can generate are described; based on this a heuristic which uses some of the methods of global program analysis and which should be capable of selecting an acceptably efficient representation automatically is given.


title: Incremental Parsing

authors:
Carlo Ghezzi
Dino Mandrioli

abstract: An incremental parser is a device which is able to perform syntax analysis in an incremental way, avoiding complete reparsing of a program after each modification. The incremental parser presented extends the conventional LR parsing algorithm and its performance is compared with that of a conventional parser. Suggestions for an implementation and possible extensions to other parsing methods are also discussed.


title: Is Sometimes Ever Better Than Alway?

abstract: The “intermittent assertion” method for proving programs correct is explained and compared with the conventional method. Simple conventional proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given.


title: Operators

abstract: Although operators, which apply to functions to produce functions, prove very useful in mathematics, they are absent from most programming languages. This paper illustrates their simplicity and power in terms of the operators of APL, and examines related constructs in other programming languages.


title: A Deterministic Attribute Grammar Evaluator Based on Dynamic Scheduling

authors:
Ken Kennedy
Jayashree Ramanathan

abstract: The problem of semantic evaluation in a compiler-generating system can be addressed by specifying language semantics in an attribute grammar [19], a context-free grammar augmented with “attributes” for the nonterminals and “semantic functions” to compute the attributes. A deterministic method for evaluating all attributes in a “semantic” parse tree is derived and shown to have time and space complexities which are essentially linear in the size of the tree. In a prepass through the parse tree, the method determines an evaluation sequence for the attributes; thus it is somewhat analogous to dynamic programming. The constructor-evaluator system described should be suitable for inclusion in a general translator-writing system.


title: Comments on "Communicating Sequential Processes"

authors:
Richard B. Kieburtz
Abraham Silberschatz

abstract: In his recent paper, “Communicating Sequential Processes” ( Comm. ACM 21, 8 (Aug. 1978), 666-677), C.A.R. Hoare outlines a programming language notation for interprocess communication in which processes are synchronized by the messages they exchange. The notation carries with it certain implications for the synchronization protocols required in a message transfer. These are not at all obvious and are made explicit here. An alternative convention is suggested in which communication and synchronization are partially uncoupled from one another.


title: A New Approach to Proving the Correctness of Multiprocess Programs

abstract: A new, nonassertional approach to proving multiprocess program correctness is described by proving the correctness of a new algorithm to solve the mutual exclusion problem. The algorithm is an improved version of the bakery algorithm. It is specified and proved correct without being decomposed into indivisible, atomic operations. This allows two different implementations for a conventional, nondistributed system. Moreover, the approach provides a sufficiently general specification of the algorithm to allow nontrivial implementations for a distributed system as well.


title: A Fast Algorithm for Finding Dominators in a Flowgraph

authors:
Thomas Lengauer
Robert Endre Tarjan

abstract: A fast algorithm for finding dominators in a flowgraph is presented. The algorithm uses depth-first search and an efficient method of computing functions defined on paths in trees. A simple implementation of the algorithm runs in O ( m log n ) time, where m is the number of edges and n is the number of vertices in the problem graph. A more sophisticated implementation runs in O ( m α( m , n )) time, where α( m , n ) is a functional inverse of Ackermann's function. Both versions of the algorithm were implemented in Algol W, a Stanford University version of Algol, and tested on an IBM 370/168. The programs were compared with an implementation by Purdom and Moore of a straightforward O ( mn )-time algorithm, and with a bit vector algorithm described by Aho and Ullman. The fast algorithm beat the straightforward algorithm and the bit vector algorithm on all but the smallest graphs tested.


title: Backtracking in a Generalized Control Setting

abstract: Backtracking is a powerful conceptual and practical programming language control structure. However, its application in general has been limited to global control over recursive programs. In this paper we explore the coherence and utility of applying backtracking in a more general control setting, namely, block-structured coroutines. The following criteria are proposed for such a control combination to be judged successful: (i) retention of each control form's individual semantics; (ii) coherent semantics for each legal application of the combination; (iii) nonpreeminence of either control form, and (iv) facilitation of genuinely novel programming effects. The attainability of these criteria is assessed, with the aid of an informal language design and three illustrative applications: (i) a dual tree walk program using coroutine-managed backtracking subsystems; (ii) a context-free language intersection tester using bilevel hierarchical backtracking, and (iii) an optimizing computer job scheduler using backtracking in a simulation language context. Full programs are given for each example, phrased in a Pascal extension offering both coroutines and backtracking (expressed through nondeterministic control).


title: Verification of Array, Record, and Pointer Operations in Pascal

authors:
David C. Luckham
Norihisa Suzuki

abstract: A practical method is presented for automating in a uniform way the verification of Pascal programs that operate on the standard Pascal data structures Array, Record, and Pointer. New assertion language primitives are introduced for describing computational effects of operations on these data structures. Axioms defining the semantics of the new primitives are given. Proof rules for standard Pascal operations on data structures are then defined using the extended assertion language. An axiomatic rule for the Pascal storage allocation operation, NEW, is also given. These rulers have been implemented in the Stanford Pascal program verifier. Examples illustrating the verification of programs which operate on list structures implemented with pointers and records are discussed. These include programs with side effects.


title: Simplification by Cooperating Decision Procedures

authors:
Greg Nelson
Derek C. Oppen

abstract: A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.


title: A Language for Array and Vector Processors

abstract: The scientific community has consistently demanded from computing machines an increase in the number of instructions executed per second. The latest increase has been achieved by duplication of arithmetic units for an array processor and the pipelining of functional units for vector processors. The high level programming languages for such machines have not benefited from the advances which have been made in programming language design and implementation techniques. A high level language is described in this paper which is appropriate for both array and vector processors and is defined without reference to the hardware of either type of machine. The syntax enables the parallel nature of a problem to be expressed in a form which can be readily exploited by these machines. This is achieved by using the data declarations to indicate the maximum extent of parallel processing and then to manipulate this, or a lesser extent, in the course of program execution. It was found to be possible to modify many of the structured programming and data structuring concepts for this type of parallel environment and to maintain the benefits of compile time and run time checking. Several special constructs and operators are also defined. The language offers to the large scale scientific computing community many of the advances which have been made in software engineering techniques while it exploits the architectural advances which have been made.


title: Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development

authors:
Noah S. Prywes
Amir Pnueli
S. Shastry

abstract: The Model II language and the associated program generator are used to explain and illustrate the use of very high level nonprocedural languages for computer programming. The effect of a very high level language is obtained in Model II through the elimination of procedural and control facilities that exist in high level programming languages such as PL/I or Cobol. In particular, the statements may be given in any order and there are no control constructs such as input/output, iterations, and memory allocation. The task of ordering the statements for execution and providing control statements is performed by the automatic program generator. The specification of a program is therefore much shorter (approximately one-fifth) than the equivalent high level procedural language program. Most important, a user need not regard the task of specifying a program as defining a process but rather as describing data and relations. This point of view greatly reduces the computer programming proficiency required of a user. The paper focuses on an example of the use of the language in business data processing, its advantages, and its novelty. It only briefly reviews the methodology incorporated in the existing program generator, a detailed description of which may be found in the references.


title: Code Generation and Storage Allocation for Machines with Span-Dependent Instructions

abstract: Many machine languages have two instruction formats, one of which allows addressing of “nearby” operands with “short” (e.g. one word) instructions, while “faraway” operands require “long” format (e.g. two words). Because the distance between an instruction and its operand depends upon the formats of the intervening instructions, the formats of different instructions may be interdependent. An efficient technique is discussed which optimally assigns formats to instructions in a given program and is practical in space as well as time. The more sophisticated problem of arranging operands within programs is discussed. Unfortunately, it is unlikely that an efficient algorithm can guarantee even a good approximation for this problem, since it is shown that r -approximation is NP-complete. Finally, implications of these problems for hardware and software design are considered.


title: The Compilation of Loop Induction Expressions

abstract: In an optimizing compiler, it is often desirable to compile subscript expressions such as Abase-2 + I*2 so that the value of the expression is available in a register and is simply incremented whenever I is incremented, thus avoiding the multiplication inside the loop. This change is effected by a standard optimization called strength reduction. Program loops often contain several such expressions stemming perhaps from references to operands A(I), A(I+1), B(I), and C(K,J,I,L). Under what circumstances can we do better than keeping four addresses in four separate registers or temporaries? A general technique is presented which minimizes the number of registers needed to hold such values, while simultaneously minimizing the amount of computation inside the loop. In the above collection, it is possible to use as few as two registers for the four I-dependent values.


title: Noncanonical SLR(1) Grammars

abstract: Two noncanonical extensions of the simple LR(1) (SLR(1)) method are presented, which reduce not only handles but also other phrases of sentential forms. A class of context-free grammars called leftmost SLR(1) (LSLR(1)) is defined by using lookahead symbols which appear in leftmost derivations. This class includes the SLR(1), reflected SMSP, and total precedence grammars as proper subclasses. The class of LSLR(1) languages properly includes the deterministic context-free languages, their reflections, and total precedence languages. By requiring that phrases which have been scanned be reduced as early as possible, a larger class of context-free grammars called noncanonical SLR(1) (NSLR(1)) is defined. The NSLR(1) languages can be recognized deterministically in linear time using a two-stack pushdown automaton. An NSLR(1) parser generator has been implemented. Empirical results show that efficient NSLR(1) parsers can be constructed for some non-LR grammars which generate nondeterministic languages. Applications of the NSLR(1) method to improve the parsing and translation of programming languages are discussed.


title: Morris's Garbage Compaction Algorithm Restores Reference Counts

abstract: The two-pass compaction algorithm of F.L. Morris, which follows upon the mark phase in a garbage collector, may be modified to recover reference counts for a hybrid storage management system. By counting the executions of two loops in that algorithm where upward and downward references, respectively, are forwarded to the relocation address of one node, we can initialize a count of active references and then update it but once. The reference count may share space with the mark bit in each node, but it may not share the additional space required in each pointer by Morris's algorithm, space which remains unused outside the garbage collector.


title: An Axiomatic Approach to Information Flow in Programs

authors:
Gregory R. Andrews
Richard P. Reitman

abstract: A new approach to information flow in sequential and parallel programs is presented. Flow proof rules that capture the information flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by examples. The applications of flow proofs to certifying information flow policies and to solving the confinement problem are considered. It is also shown that flow rules and correctness rules can be combined to form an even more powerful proof system.


title: A Proof System for Communicating Sequential Processes

authors:
Krzysztof R. Apt
Nissim Francez
Willem P. de Roever

abstract: An axiomatic proof system is presented for proving partial correctness and absence of deadlock (and failure) of communicating sequential processes. The key (meta) rule introduces cooperation between proofs, a new concept needed to deal with proofs about synchronization by message passing. CSP's new convention for distributed termination of loops is dealt with. Applications of the method involve correctness proofs for two algorithms, one for distributed partitioning of sets, the other for distributed computation of the greatest common divisor of n numbers.


title: Uniform Random Generation of Balanced Parenthesis Strings

authors:
D. B. Arnold
M. Ronan Sleep

abstract: The empirical testing of error repair schemes for skeletons of source programs in a block-structured language leads to the problem of generating balanced parenthesis strings in a uniform random manner. An efficient generator which works from left to right must compute the correct probability for the next symbol at each stage of the generation. The associated enumeration problem may be solved by adopting a geometric interpretation usually associated with random walk problems. This solution leads immediately to an O ( n ) algorithm for the generator.


title: Output Guards and Nondeterminism in "Communicating Sequential Processes"

abstract: In a recent paper C.A.R. Hoare outlined a language for concurrent programming. Guarded commands and nondeterminism are two features of the language. This paper points out two problems that arise in connection with these features and addresses one of them.


title: Managing Reentrant Structures Using Reference Counts

abstract: Automatic storage management requires that one identify storage unreachable by a user's program and return it to free status. One technique maintains a count of the references from user's programs to each cell, since a count of zero implies the storage is unreachable. Reentrant structures are self-referencing; hence no cell in them will have a count of zero, even though the entire structure is unreachable. A modification of standard reference counting can be used to manaage the deallocation of a large class of frequently used reentrant structures, including two-way and circularly linked lists. All the cells of a potentially reentrant structure are considered as part of a single group for deallocation purposes. Information associated with each cell specifies its group membership. Internal references (pointers from one cell of the group to another) are not reference counted. External references to any cell of this group are counted as references to the group as a whole. When the external reference count goes to zero, all the cells of the group can be deallocated. This paper describes several ways of specifying group membership, properties of each implementation, and properties of mutable and immutable group membership.


title: Derivation of Invariant Assertions During Program Development by Transformation

authors:
Manfred Broy
Bernd Krieg-Brückner

abstract: Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.


title: A Formal System for Reasoning about Programs Accessing a Relational Database

authors:
Marco A. Casanova
Philip A. Bernstein

abstract: A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definition language (DDL) for describing relational databases and a data manipulation language (DML) whose programs access data in a database. The DDL is a many-sorted first-order language that accounts for data aggregations. The DML features a many-sorted assignment in place of the usual data manipulation statements, in addition to the normal programming language constructs.


title: Automatic Derivation of Code Generators from Machine Descriptions

abstract: Work with compiler compilers has dealt principally with automatic generation of parsers and lexical analyzers. Until recently, little work has been done on formalizing and generating the back end of a compiler, particularly an optimizing compiler. This paper describes formalizations of machines and code generators and describes a scheme for the automatic derivation of code generators from machine descriptions. It was possible to separate all machine dependence from the code generation algorithms for a wide range of typical architectures (IBM-360, PDP-11, PDP-10, Intel 8080) while retaining good code quality. Heuristic search methods from work in artificial intelligence were found to be both fast and general enough for use in generation of code generators with the machine representation proposed. A scheme is proposed to perform as much analysis as possible at code generator generation time, resulting in a fast pattern-matching code generator. The algorithms and representations were implemented to test their practicality in use.


title: Synthesis of Resource Invariants for Concurrent Programs

abstract: Owicki and Gries have developed a proof system for conditional critical regions . In their system, logically related variables accessed by more than one process are grouped together as resources , and processes are allowed access to a resource only in a critical region for that resource. Proofs of synchronization properties are constructed by devising predicates called resource invariants which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants. Methods are developed in this paper for automatically synthesizing resource invariants. Specifically, the resource invariants of a concurrent program are characterized as least fixpoints of a functional which can be obtained from the text of the program. By the use of this fixpoint characterization and a widening operator based on convex closure, good approximations may be obtained for the resource invariants of many concurrent programs.


title: A Note on Median Split Trees

abstract: The median split tree is an elegant technique for searching static sets of keys when the frequency of access is highly skewed. This paper generalizes the median split search technique, relates it to sequential search and binary search, discusses the choice of an optimum search strategy for a given set of keys, and poses several related optimization problems.


title: The Design and Application of a Retargetable Peephole Optimizer

authors:
Jack W. Davidson
Christopher W. Fraser

abstract: Peephole optimizers improve object code by replacing certain sequences of instructions with better sequences. This paper describes PO, a peephole optimizer that uses a symbolic machine description to simulate pairs of adjacent instructions, replacing them, where possible, with an equivalent single instruction. As a result of this organization, PO is machine independent and can be described formally and concisely: when PO is finished, no instruction, and no pair of adjacent instructions, can be replaced with a cheaper single instruction that has the same effect. This thoroughness allows PO to relieve code generators of much case analysis; for example, they might produce only load/add-register sequences and rely on PO to, where possible, discard them in favor or add-memory, add-immediate, or increment instructions. Experiments indicate that naive code generators can give good code if used with PO.


title: Specification of Abstract Data Types in Modula

authors:
George W. Ernst
William F. Ogden

abstract: The programming language MODULA is extended to permit the formal specification of the structure and functional capabilities of modules. This makes true hierarchical programming possible in MODULA by allowing programmers of higher level parts of a system to ignore completely the internal structure of lower level modules and to rely entirely on the specifications of the capabilities of these modules. An example is included to illustrate this technique. We show that our specification mechanisms are sufficiently powerful to support formal verification rules for modules that have disjoint representations for abstract objects.


title: On Parsing and Compiling Arithmetic Expressions on Vector Computers

abstract: The problem of parsing and compiling arithmetic expressions on vector computers is considered. Methods are developed which allow encodings of one or more arithmetic expressions to be transformed directly into encodings of their corresponding derivation trees. The algorithm which performs this transformation is compact, efficient, and able to make extensive use of concurrent vector operations. Routines which concurrently transverse encoded derivation trees in a top-down or bottom-up manner are presented. These routines can be used to structure efficient, compact, and highly concurrent algorithms which complete the process of compiling arithmetic expressions.


title: Distributed Termination

abstract: Discussed is a distributed system based on communication among disjoint processes, where each process is capable of achieving a post-condition of its local space in such a way that the conjunction of local post-conditions implies a global post-condition of the whole system. The system is then augmented with extra control communication in order to achieve distributed termination, without adding new channels of communication. The algorithm is applied to a problem of constructing a sorted partition.


title: An Improved Context-Free Recognizer

authors:
Susan L. Graham
Michael A. Harrison
Walter L. Ruzzo

abstract: A new algorithm for recognizing and parsing arbitrary context-free languages is presented, and several new results are given on the computational complexity of these problems. The new algorithm is of both practical and theoretical interest. It is conceptually simple and allows a variety of efficient implementations, which are worked out in detail. Two versions are given which run in faster than cubic time. Surprisingly close connections between the Cocke-Kasami-Younger and Earley algorithms are established which reveal that the two algorithms are “almost” identical.


title: Assignment and Procedure Call Proof Rules

authors:
David Gries
Gary Levin

abstract: The multiple assignment statement is defined in full generality—including assignment to subscripted variables and record fields—using the “axiomatic” approach of Hoare. Proof rules are developed for calls of procedures using global variables, var parameters, result parameters, and value parameters, using the idea of multiple assignment to provide understanding. An attempt is made to clarify some issues that have arisen concerning the use of rules of inference to aid in generating “verification conditions” in mechanical verifiers and the use of logical variables to denote initial values of program variables.


title: An Alternative to the Use of Patterns in String Processing

authors:
Ralph E. Griswold
David R. Hanson

abstract: SNOBOL4 is best known for its string processing facilities, which are based on patterns as data objects. Despite the demonstrated success of patterns, there are many shortcomings associated with their use. The concept of patterns in SNOBOL4 is examined and problem areas are discussed. An alternative method for high-level string processing is described. This method, implemented in the programming language Icon, employs generators , which are capable of producing alternative values. Generators, coupled with a goal-driven method of expression evaluation, provide the string processing facilities of SNOBOL4 without the disadvantages associated with patterns. Comparisons between SNOBOL4 and Icon are included and the broader implications of the new approach are discussed.


title: And/Or Programs: A New Approach to Structured Programming

abstract: A simple tree-like programming/specification language is presented. The central idea is the dividing of conventional programming constructs into the two classes of and and or subgoaling, the subgoal tree itself constituting the program. Programs written in the language can, in general, be both nondeterministic and parallel. The syntax and semantics of the language are defined, a method for verifying programs written in it is described, and the practical significance of programming in the language assessed. Finally, some directions for further research are indicated.


title: Applicability of Software Validation Techniques to Scientific Programs

abstract: Error analysis involves the examination of a collection of programs whose errors are known. Each error is analyzed and validation techniques which would discover the error are identified. The errors that were present in version five of a package of Fortran scientific subroutines and then later corrected in version six were analyzed. An integrated collection of static and dynamic analysis methods would have discovered the errors in version five before its release. An integrated approach to validation and the effectiveness of individual methods are discussed.


title: An Abstract Type for Statistics Collection in Simula

abstract: Although the use of abstract types has been widely advocated as a specification and implementation technique, their use has often been associated with programming languages that are not widely available, and examples published to date are rarely taken from actual applications. SIMULA is a widely available language that supports the use of abstract types. The purposes of this paper are (1) to demonstrate the application of the concepts of data abstraction to a common problem; (2) to demonstrate the use of data abstraction in a widely available language; and (3) to provide a portable facility for statistics collection that may make the use of SIMULA more attractive. A discussion of the background of and requirements for an abstract type for statistics collection is presented, followed by a specification for the type using traces. A SIMULA implementation, with examples of its use, is given. Finally, implementation of the abstract type in other languages is discussed.


title: Chaining Span-Dependent Jump Instructions

authors:
Bruce W. Leverett
Thomas G. Szymanski

abstract: The assembled length of a span-dependent jump instruction depends on the distance between the instruction and its target. Such instructions are found on many computers and typically have two forms, long and short. We consider the problem of minimizing object program length for such machines by chaining together jumps with the same target. Although the problem is NP-complete in its most general form, several mildly restricted forms of the problem exist that are of practical importance and have efficient solutions.


title: Ada Exception Handling: An Axiomatic Approach

authors:
David C. Luckham
Wolfgang Polak

abstract: A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analyzed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e., nonerror situations). Example verifications are given.


title: Design of a Machine-Independent Optimizing System for Emulator Development

authors:
Perng-Yi Richard Ma
Ted G. Lewis

abstract: Methods are described to translate a certain machine-independent intermediate language (IML) to efficient microprograms for a class of horizontal microprogrammable machines. The IML is compiled directly from a high-level microprogramming language used to implement a virtual instruction set processor as a microprogram. The primary objective of the IML-to-host machine interface design is to facilitate language portability. Transportability is accomplished by use of a field description model and a macro expansion table which describe the host machine to the translator system. Register allocation scheme and control flow analysis are employed to allocate the symbolic variables of the IML to the general-purpose registers of the host machine. A set of 5-tuple microoperations (function, input, output, field, phase) is obtained with the aid of the field description model. Then a compaction algorithm is used to detect the parallelism of microoperations and to generate suboptimal code for a horizontal microprogrammable machine. The study concludes with a description of the effects of the above methods upon the quality of microcode produced for a specific commercial computer.


title: A Deductive Approach to Program Synthesis

authors:
Zohar Manna
Richard J. Waldinger

abstract: Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.


title: The Activity of a Variable and Its Relation to Decision Trees

authors:
Bernard M. E. Moret
Michael G. Thomason
Rafael C. González

abstract: The construction of sequential testing procedures from functions of discrete arguments is a common problem in switching theory, software engineering, pattern recognition, and management. The concept of the activity of an argument is introduced, and a theorem is proved which relates it to the expected testing cost of the most general type of decision trees. This result is then extended to trees constructed from relations on finite sets and to decision procedures with cycles. These results are used, in turn, as the basis for a fast heuristic selection rule for constructing testing procedures. Finally, some bounds on the performance of the selection rule are developed.


title: Prettyprinting

abstract: An algorithm for prettyprinting is given. For an input stream of length n and an output device with linewidth m , the algorithm requires time O ( n ) and space O ( m ). The algorithm is described in terms of two parallel processes: the first scans the input stream to determine the space required to print logical blocks of tokens; the second uses this information to decide where to break lines of text; the two processes communicate by means of a buffer of size O ( m ). The algorithm does not wait for the entire stream to be input, but begins printing as soon as it has received a full line of input. The algorithm is easily implemented.


title: Global Context Recovery: A New Strategy for Syntactic Error Recovery by Table-Drive Parsers

authors:
Ajit B. Pai
Richard B. Kieburtz

abstract: Described is a method for syntactic error recovery that is compatible with deterministic parsing methods and that is able to recover from many errors more quickly than do other schemes because it performs global context recovery. The method relies on fiducial symbols, which are typically reserved key words of a language, to provide mileposts for error recovery. The method has been applied to LL(1) parsers, for which a detailed algorithm is given, and informally proved correct. The algorithm will always recover and return control to the parser if the text being analyzed satisfies only minimal requirements: that it contains one or more occurrences of fiducial symbols following the point at which an error is detected. Tables needed for error recovery have been automatically generated, along with parsing tables, by a parser constructor for the LL(1) grammars. A theoretical characterization of fiducial symbols is given, and the utility of this characterization in practice is discussed. It has been applied to a grammar for the programming language Pascal to aid in selection of a set of fiducial symbols. The error recovery scheme has been tested on a set of student-written Pascal program texts and is compared with other error recovery strategies.


title: On the Performance of Balanced Hashing Functions When the Keys Are Not Equiprobable

authors:
Christos H. Papadimitriou
Philip A. Bernstein

abstract: The cost (expected number of accesses per retrieval) of hashing functions is examined without the assumption that it is equally probable for all keys to be present in the table. It is shown that the obvious strategy—trying to balance the sums of probabilities of the keys mapped to any given address—may be suboptimal; however, the difference from the exactly optimal distribution cannot be large.


title: A Coroutine Approach to Parsing

abstract: A method is presented for parsing syntactic constructs that are permitted to appear independently anywhere in a program. Some examples include comments, macros, and constructs for conditional compilation. Each such construct is defined by its own grammar and parsed by a separate coroutine. The coroutine model of parsing allows the program text to be parsed in one pass despite the syntactic inconsistencies among the program text and the additional constructs. The usefulness of the model is demonstrated by showing how a production language parsing method is extended to handle multiple syntax specifications. The implementation of conditional compilation by carrying along two parses in a coroutine manner is also given. The utility of the model is further demonstrated by showing its adaptation to a recursive descent parser.


title: Ultracomputers

abstract: A class of parallel processors potentially involving thousands of individual processing elements is described. The architecture is based on the perfect shuffle connection and has two favorable characteristics: (1) Each processor communicates with a fixed number of other processors. (2) Important communication functions can be accomplished in time proportional to the logarithm of the number of processors. A number of basic algorithms for these “ultracomputers” are presented, and physical design considerations are discussed in a preliminary fashion.


title: External Representations of Objects of User-Defined Type

abstract: The portable programming language (PPL) is one of a number of recently designed programming languages that enable the user to define new types by giving their representations and operations in terms of those of previously available types. Such provisions for the construction of objects of user-defined type have been discussed elsewhere; this work concerns the related problem of the external representations of such objects, both on input-output media and as written constants within the program text. We introduce an enhancement to the PPL design allowing specification of the external representations of objects of user-defined type. This extension to the PPL design means that objects of user-defined type can be read, written, and used as constants exactly as if their representations had been selected by the writer of the PPL compiler. The implementation and use of the added facilities are also discussed.


title: Locally Least-Cost Error Recovery in Early's Algorithm

authors:
Stuart Oliver Anderson
Roland Carl Backhouse

abstract: ~While-least-cost~ error correction is fundamentally important to context-free language processing, it is inefficient w'Qhemdone globally.A locally least-cost repair method has been devised to model error recovery in conventional-~o-mpile]ts.The principles of this recovery technique have inspired a practical LL(1) method and should be of value m ~ntmg-error~rJel~a~lr m other parsing algorithms.-At each point in the syntax analysis, a locally optimal repair of't~e-next-sy-mBffl is defined to be a string w such that w can be parsed without error and such that editing the symbol following w can be achieved at least cost, costs being defined by the Wagner-Fischer model of string-to-string correction.In this paper we describe how error recovery can be achieved in Earley's algorithm by simulating locally optimal repairs.The main result is to show that the complexity of Earley's algorithm is not affected by this process; that is, for any input string of length n, the work involved is O(n) if the given grammar is deterministic, O(n 2) if the grammar is unambiguous, and O(n 3) in the worst case.Key Words and Phrases: error repair,


authors:
F. André
Jean-Pierre Banâtre
Jean-Paul Routeau

abstract: article Free Access Share on A Multiprocessing Approach to Compile-Time Symbol Resolution Authors: F. André Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, France Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, FranceView Profile , J. P. Banatre Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, France Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, FranceView Profile , J. P. Routeau Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, France Institut de recherche en informatique et systèmes aléatoires (IRISA), Campus de Beaulieu, Avenue du General Leclerc, 35042--Rennes Cédex, FranceView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 1Jan. 1981 pp 11–23https://doi.org/10.1145/357121.357123Online:01 January 1981Publication History 4citation215DownloadsMetricsTotal Citations4Total Downloads215Last 12 Months4Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Synchronizing Resources

abstract: A new proposal for synchronization and communication in parallel programs is presented.The proposal synthesizes and extends aspects of procedures, coroutines, critical regions, messages, and monitors.It provides a single notation for parallel programming with or without shared variables and is suited for either shared or distributed memory architectures.The essential new concepts are operations, input statements, and resources.The proposal is illustrated by the solutions of a variety of parallel programming problems; its relation to other parallel programming proposals is also discussed.


title: Ten Years of Hoare's Logic: A Survey - Part 1

abstract: A survey of various results concerning Hoare's approach to proving partial and total correctness of programs is presented.Emphasis is placed on the soundness and completeness issues.Various proof systems for while programs, recursive procedures, local variable declarations, and procedures with parameters, together with the corresponding soundness, completeness, and incompleteness results, are discussed.


title: Nonsequentiality and Concrete Activity Phases in Discrete-Event Simulation Languages

abstract: The design of languages for programming complex discrete-event simulations, with a conventional global notion of simulation time, is considered.An example language is described in which the main objects dealt with are concrete manifestations of phases of activity conceptually underlying a simulation and in which programs have an extremely nonsequential mode of notional operation.A program in the language very directly specifies a certain type of formal simulation system which generates a unique maximal simulation history.This history is a sequence of time instants, each associated with the partially ordered set of events considered to occur at that instant.In contrast to the case of programs in existing discrete-event simulation languages, (1) the event orders achievable at instants can be partial and are not restricted in any way, and (2) phase objects are central and explicit in a program, being the main units describing overall structure, data, and control.Variants of the language could have uses other than simulation.


abstract: article Free Access Share on The Programming Language Aspects of ThingLab, a Constraint-Oriented Simulation Laboratory Author: Alan Borning Department of Computer Science, FR-35, University of Washington, Seattle, WA Department of Computer Science, FR-35, University of Washington, Seattle, WAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 4Oct. 1981 pp 353–387https://doi.org/10.1145/357146.357147Published:01 October 1981Publication History 570citation1,242DownloadsMetricsTotal Citations570Total Downloads1,242Last 12 Months119Last 6 weeks41 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Process Communication Based on Input Specifications

authors:
Jan van den Bos
Marinus J. Plasmeijer
Jan Stroet

abstract: InputInput tools, originally introduced as a language model for interactive systems and based on high-level, input-driven objects, have been developed into a model for communicating parallel processes, called the input tool process model (ITP).In this model every process contains an input rule, comparable to the right-hand side of a production rule.This rule specifies in an expression the patterns and sources of input it exPects and where the input is to be handled.The reception of the input triggers action inside the too! process.As part of the action, messages may be sent to other processes, with destination specified to a varying degree of identification.A potential candidate for a message is any tool process with the correct type of message slot.Because sending tool processes do not have to specify completely the identity of receiving tool processes, and vice versa, ITP provides a fully dynamic communication model.Most communication aspects of other recently developed models are contained in this model.Synchronization of processes is accomplished implicitly by the input specification; explicit synchro-nizatiQn constructs such as monitors and guarded regions can therefore be easily simulated.The ITP constructs provide a general concept for interprocess communication.Its application areas range from interaction via process control to operating systems.From a programming point of view, the language constructs offered are not in any way dependent on whether processes run on single or multiple processors.


title: Editing Data Structures

authors:
Christopher W. Fraser
A. A. Lopez

abstract: Text is not the only data that needs editing.For example, interactive debuggers edit data structures internal to running programs.This paper describes eds, a generalized editor that allows users to edit arbitrary data structures.Examples show eds maintaining simple databases, editing LISP S-expressions, debugging SNOBOL4 programs, and creating and modifying data structures for a computer graphics system.


title: Data-Abstraction Implementation, Specification, and Testing

authors:
John D. Gannon
Paul R. McMullin
Richard G. Hamlet

abstract: A compiler-based system DAISTS that combines a data-abstraction implementation language (derived from the SIMULA class) with specification by algebraic axioms is described.The compiler, presented with two independent syntactic objects in the axioms and implementing code, compiles a "program" that consists of the former as test driver for the latter.Data points, in the form of expressions using the abstract functions and constant values, are fed to this program to determine if the implementation and axioms agree.Along the way, structural testing measures can be applied to both code and axioms to evaluate the test data.Although a successful test does not conclusively demonstrate the consistency of axioms and code, in practice the tests are seldom successful, revealing errors.The advantage over conventional programming systems is threefold:(1) The presence of the axioms eliminates the need for a test oracle; only inputs need be supplied.(2) Testing is automated: a user writes axioms, implementation, and test points; the system writes the test drivers.(3) The results of tests are often surprising and helpful because it is difficult to get away with "trivial" tests: what is not significant for the code is liable to be a severe test of the axioms, and vice versa.


title: Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer

authors:
Irene Greif
Albert R. Meyer

abstract: We consider three kinds of mathematical objects which can be designated as the "meaning" or "semantics" of programs: binary relations between initial and final states, binary relations on predicates (partial-correctness semantics), and functionals from predicates to predicates (predicate transformers).We exhibit various formal specification mechanisms: induction on program syntax, axioms, and deductive systems.We show that each kind of semantics can be specified by several different mechanisms.As long as arbitrary predicates on states are permitted, each kind of semantics uniquely determines the others, with the sole exception of the weakest precondition semantics for nondeterministic programs.


title: Generators in Icon

authors:
Ralph E. Griswold
David R. Hanson
John T. Korb

abstract: Icon is a new programming language that includes a goal-directed expression evaluation mechanism.This mechanism is based on generators--expressions that are capable of producing more than one value.If the value produced by a generator does not lead to a successful result, the generator is automatically activated for an alternate value.Generators form an integral part of Icon and can be used anywhere.In addition, they form the basis for the string scanning facility and subsume some of the control expressions found in other languages.Several examples are given.


title: Deleting Irrelevant Tasks in an Expression-Oriented Multiprocessor System

authors:
Dale H. Grit
Rex L. Page

abstract: Parallelism gleaned from concurrent evaluation of subexpressions in a multiprocessor designed for parallel evaluation of recursive programs can lead to the generation of unnecessary computations.Even when these unnecessary computations do not threaten to overwhelm the system, it may be worth devoting some resources to terminating them.A method for deleting irrelevant processes without temporarily suspending the overall computation is described, especially as it relates to a particular model for a multiprocessor system designed to evaluate expressions by a computation rule related to "full substitution."


title: A Cost Model for the Internal Organization of B+-Tree Nodes


title: Algorithm 568: PDS - A Portable Directory System

abstract: PDS is a set of procedures that provides a machine-independent method of file specification.PDS provides capabilities beyond those provided by many vendorsupplied systems.In addition, because PDS is portable, additional capabilities, such as protection schemes, file usage statistics, or some of the functions of a source code control system [5], can be added easily.The basic function of PDS is to maintain a useful directory structure and provide a set of primitives for manipulating that structure.The PDS directory structure is identical to the tree structure of the UNIX [4] file system, and many of the PDS primitives are identical to UNIX primitives.PDS is, in large part, a portable implementation of the UNIX directory system.Besides PDS's machineindependence, the major differences are the extensibility of PDS and, as described in the next section, its i/o independence.In the simplest terms, PDS provides a directory structure and a mapping from machine-independent file names to machine-dependent names.It deals only with the information describing a file; it does not use or manipulate actual files in any way.The importance of this approach is that PDS is used to specify a file but does not participate in the actual i/o to that file.Consequently, there is no impact on i/o efficiency when PDS is used.PDS manipulates a rooted tree structure in which the leaves are files or directories and the nodes are directories.A directory is simply a list of files and directories.An example is shown in Figure 1, in which circles indicate directories and squares indicate files.The root of the tree is denoted by "/", and files and directories are denoted by their "path," which specifies their absolute position in the tree.A path is composed of the names of the nodes on the path from the root


title: Space-Efficient Storage Management in an Attribute Grammar Evaluator

authors:
Mehdi Jazayeri
Diane Pozefsky

abstract: A space-efficient strategy for storing attributes during evaluation of an attribute grammar is presented.Attributes are classified as either one-pass or multipass.One-pass attributes are stored on a pushdown stack, and their storage is freed when no longer needed.Examination of extant grammars shows that a vast majority of attributes are indeed one-pass, and therefore the scheme presented can greatly reduce the storage requirements of an attribute grammar evaluator.Several approaches to storage management for multipass attributes are also presented.Data for several grammars are collected and used to show the effectiveness of the proposed storage management scheme.


authors:
Otto C. Juelich
Clinton R. Foulk

abstract: article Free Access Share on Compilation of Acyclic Smooth Programs for Parallel Execution Authors: Otto C. Juelich Missile Systems Division, Rockwell International, Columbus, OH Missile Systems Division, Rockwell International, Columbus, OHView Profile , Clinton R. Foulk Department of Computer and Information Science, The Ohio State University, 2036 Neil Avenue Mall, Columbus, OH Department of Computer and Information Science, The Ohio State University, 2036 Neil Avenue Mall, Columbus, OHView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 1Jan. 1981 pp 24–48https://doi.org/10.1145/357121.357124Published:01 January 1981Publication History 1citation201DownloadsMetricsTotal Citations1Total Downloads201Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Methods for Computing LALR(k) Lookahead

authors:
Bent Bruun Kristensen
Ole Lehrmann Madsen


title: The Construction of Stack-Controlling LR Parsers for Regular Right Part Grammars

abstract: Although determinisitic pushdown automata and LR(k) parsers are formally equivalent, the latter (unlike the former) stack one symbol for each input symbol read.By relaxing this requirement, we obtain a class of LR parsers that can perform finite state recognition locally without associated stack manipulations.The definition and construction of such stack-controlling LR parsers is examined in detail along with some potential application areas.


title: Handling Operator Precedence in Arithmetic Expressions with Tree Transformations

authors:
Wilf R. LaLonde
Jim des Rivières

abstract: A simple linear time and space algorithm that transforms a standardized tree representation of an arithmetic expression lacking operator precedence information into a tree containing it is presented.The approach has applications in modularizing compilers, since the transformations can be applied after the parsing phase.Moreover, it facilitates the compiling of languages that allow dynamic operator definition.


title: Referencing and Retention in Block-Structured Coroutines

authors:
Gary Lindstrom
Mary Lou Soffa

abstract: The combination of coroutines with recursive procedures is characteristic of many modern higher level languages offering advanced control structures (e.g., SIMULA-67, SL5, or INTERLISP). We say a language has block-structured coroutines (BSCRs) when static nesting considerations govern the usage of this control combination. Starting with the BSCR control description work of Wang and Dahl, this paper pursues further the implications of static program structure on BSCR programs in a particular compilation-oriented setting. Disciplines on BSCR reference assignment and individual control actions are defined, offering enhanced implementability and program comprehensibility. Of particular interest is a scope-based discipline on "detach " operations, which avoids the formation of idle chain subheads, an implementationally undesirable condition. The retention requirements of BSCRs are analyzed under a range of possible remote accessibility conditions, and two deletion strategies are then defined, keyed to these requirements. The first uses a special form of scope-sensitive reference counting, and the second does mark-sweep garbage collection, again exploiting static program structure. Space and time estimates for both methods are given, along with avenues for continuing research.


title: An Exercise in Program Explanation

abstract: article An Exercise in Program Explanation Share on Author: Jayadev Misra Department of Computer Sciences, College of Natural Sciences, The University of Texas at Austin, Austin, TX Department of Computer Sciences, College of Natural Sciences, The University of Texas at Austin, Austin, TXView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 1Jan. 1981 pp 104–109https://doi.org/10.1145/357121.357128Published:01 January 1981 4citation294DownloadsMetricsTotal Citations4Total Downloads294Last 12 Months6Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Associons: A Program Notation with Tuples Instead of Variables

abstract: A program notation without variables is proposed.The state of a computation is recorded as a set of "associons."Each associon is a tuple of names representing a relation between the entities with those names.The state of the computation can be changed by the creation of new associons representing new relations deducible from those already recorded.The building block prescribing such deductions is called the "closure statement."The notation proposed is the result of our search for a basic statement the execution of which may employ more concurrency than is the case for the traditional assignment statement.Some possible extensions to the notation are discussed.


title: An Automatic Technique for Selection of Data Structures in SETL Programs

authors:
Edmond Schonberg
Jacob T. Schwartz
Micha Sharir

abstract: SETL is a very-high-level programming language supporting set-theoretic syntax and semantics.It allows algorithms to be programmed rapidly and succinctly without requiring data-structure declarations to be supplied.Such declarations can be manually specified later, without recoding the program, to improve the efficiency of program execution.We describe a new technique for automatic selection of appropriate data representations during compile time for programs with omitted declarations and present an efficient data representation selection algorithm, whose complexity is comparable with those of the fastest known general data-flow algorithms of Tarjan and Reif.


abstract: article Free Access Share on A Statement-Oriented Approach to Data Abstraction Author: J. Steensgaard-Madsen DIKU, Sigurdsgade 41, DK-2200 Copenhagen N, Denmark DIKU, Sigurdsgade 41, DK-2200 Copenhagen N, DenmarkView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 1Jan. 1981 pp 1–10https://doi.org/10.1145/357121.357122Published:01 January 1981Publication History 8citation211DownloadsMetricsTotal Citations8Total Downloads211Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Some Techniques for Recursion Removal from Recursive Programs

authors:
Jacques J. Arsac
Yves Kodratoff

abstract: RemovalThree different techniques that can be used for recursion removal are described: generalization of the function definition, study of the computation traces of the function, and nonprocedural languages.Despite the existence of implemented versions of these techniques, they are easy to use "by hand" and should therefore be part of every programmer's knowledge.


title: R/ for Semantics

authors:
Edward A. Ashcroft
William W. Wadge

abstract: A constructive criticism of recent work in the semantics of programming languages is offered.The criticism is directed not so much at the techniques and results obtained as at the use to which they are put.The fact that denotational (or "mathematical") semantics plays on the whole a passive ("descriptive") role, whil e operational semantics plays on the whole an active ("prescriptive") role, is seen as the basic problem.It is suggested that these roles be reversed.


title: A One-Pass Algorithm for Overload Resolution in Ada

abstract: OverloadA simple method is presented for detecting ambiguities and finding the correct interpretations of expressions in the programming language Ada.Unlike previously reported solutions to this problem, which require multiple passes over a tree structure, the method described here operates in one bottom-up pass, during which a directed acyclic graph is produced.The correctness of this approach is demonstrated by a brief formal argument.


title: A Structured APL System

authors:
J. Bergeron
A. Dubuque

abstract: A structured APL system introducing several interesting features is described.The APL group concept has been considerably extended to yield a new type of APL object called a segment.Segments constitute the basic building blocks used to manage memory and to build up the workspace and the user's library.The encapsulation capability provides a unified scheme for handling variables, functions, and other APL objects, including fries.A new structured user library is proposed.The dynamic call of objects during a terminal session links the user library to the workspace.New types of variables are described along with solutions to interesting problems based on them.


title: A Weaker Precondition for Loops

abstract: article Free Access Share on A Weaker Precondition for Loops Author: H. J. Boom Computer Science Department, Concordia University, 1455 de Maisonneuve Boulevard West, Montreal, P.Q., Canada H3G 1M8 Computer Science Department, Concordia University, 1455 de Maisonneuve Boulevard West, Montreal, P.Q., Canada H3G 1M8View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 4Issue 4Oct. 1982 pp 668–677https://doi.org/10.1145/69622.357189Published:01 October 1982Publication History 26citation454DownloadsMetricsTotal Citations26Total Downloads454Last 12 Months33Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Combining Algebraic and Algorithmic Reasoning: An Approach to the Schorr-Waite Algorithm

authors:
Manfred Broy
Peter Pepper

abstract: The basic idea of the Schorr-Waite graph-marking algorithm can be precisely formulated, explained, and verified in a completely applicative (functional) programming style.Graphs are specified algebraically as objects of an abstract data type.When formulating recursive programs over such types, one can combine algebraic and algorithmic reasoning: An applicative depth-first-search algorithm is derived from a mathematical specification by applying properties of reflexive, transitive closures of relations.This program is then transformed in several steps into a fmal procedural version with the help of both algebraic properties of graphs and algorithmic properties reflected in the recursion structure of the program.


authors:
Frank DeRemer
Thomas J. Pennello

abstract: article Free Access Share on Efficient Computation of LALR(1) Look-Ahead Sets Authors: Frank DeRemer Computer and Information Sciences, University of California, Santa Cruz, CA Computer and Information Sciences, University of California, Santa Cruz, CAView Profile , Thomas Pennello Computer and Information Sciences, University of California, Santa Cruz, CA Computer and Information Sciences, University of California, Santa Cruz, CAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 4Issue 4Oct. 1982 pp 615–649https://doi.org/10.1145/69622.357187Published:01 October 1982Publication History 83citation2,258DownloadsMetricsTotal Citations83Total Downloads2,258Last 12 Months471Last 6 weeks49 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Transformational Derivation of a Garbage Collection Algorithm

authors:
Robert B. K. Dewar
Micha Sharir
Elia Weixelbaum

abstract: Transformational programming is a relatively new programming technique intended to derive complex algorithms automatically.Initially, a set of transformational rules is described, and an initial specification of the problem to be programmed is given.The specification is written in a high-level language in a fairly compact form possibly ignoring efficiency.A number of versions, called transformations, are created by successively applying the transformational rules starting with the initial specification.As an example of the application of this technique to a fairly complex case, a transformational derivation of a variant of a known efficient garbage collection and compaction algorithm from an initial very high-level specification is given.Currently, the techniques are still being developed, and therefore the transformations are derived manually.However, most of the transformations done are of a technical nature and could eventually be automated.


title: High-Level Language Implications of the Proposed IEEE Floating-Point Standard

abstract: An IEEE Computer Society working group on floating-point arithmetic has recommended a standard for binary floating.pointnumber formats, operations, and semantics.This paper, which has evolved in part during the deliberations of that committee, describes the significance to languages and, in particular, to FORTRAN and its Variants, of various novel features of the recommended standard.