Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL approach that improves the localization of a given SBFL base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that better localize the individual faults in the system. This allows it to identify and re-rank faults ranked too low by the base metric because they were masked by other program elements. Through this process, FLITSR returns a set of highly suspicious program elements (called a basis), where the execution of each failing test involves at least one basis element, considered as the cause of the failure. We implemented the FLITSR algorithm in an open source toolset and extensively evaluated it over three true multi-fault datasets, varying the fault type, coverage granularity and programming language. Our evaluation shows that FLITSR consistently outperforms existing localization metrics and methods, including those designed to handle multiple faults such as ARTEMIS and parallel debugging. For the Defects4J method-level faults, FLITSR also substantially outperforms GRACE, a state-of-the-art learning-based fault localizer.

This report details the contents of the artifact for the paper “FLITSR: Improved Spectrum-Based Localization of Multiple Faults by Iterative Test Suite Reduction,” as well as detailed instructions for its installation and usage. The artifact contains all the necessary components to replicate the results of the study, including the three datasets used as well as the FLITSR tool which is used as both the implementation of the FLITSR algorithm and the evaluation framework for the experiments in the study.

Software fault datasets such as Defects4J provide for each individual fault its location and repair, but do not characterize the faults. Current classifications use the repairs as proxies, but these do not capture the intrinsic nature of the fault. In this paper, we propose a new, direct fault classification scheme based on the control- and data-flow graph representations of programs. Our scheme comprises six control-flow and two data-flow fault classes. We manually apply this scheme to 488 faults from seven projects in the Defects4J dataset. We find that the majority of the faults are assigned between one and three classes. We also find that one of the data-flow fault classes (definition fault) is the most common individual class but that the majority of faults are classified with at least one control-flow fault class. Our proposed classification can be applied to other fault datasets and can be used to improve fault localization and automated program repair techniques for specific fault classes.

Datasets such as Defects4J and BugsInPy that contain bugs from real-world software projects are necessary for a realistic evaluation of automated debugging tools. However, these datasets largely identify only a single bug in each entry, while real-world software projects (including those used in Defects4J and BugsInPy) typically contain multiple bugs at the same time. We lift this limitation and describe an automated approach to identify multiple existing bugs in the individual dataset entries. We use test case transplantation and fault location translation to expose and locate the bugs, respectively. We identified 9.2 faults on average in each of the 311 versions of the 5 projects in Defects4J, and 18.6 faults in 501 versions of the 17 projects in BugsInPy. We thus provide datasets of true multi-fault versions within real-world software projects, which maintain the properties, format and usability of the original datasets.

We describe and evaluate spectrum-based methods aimed at finding faults in context-free grammars. In their basic form, they take as input a test suite and a parser for the grammar that is modified to collect grammar spectra (i.e., the sets of grammar elements used in attempts to parse the individual test cases), and return as output a ranked list of suspicious elements. We define grammar spectra suitable for localizing faults on the level of the grammar rules (i.e., rule spectra) and the rules’ individual symbols (i.e., item spectra), respectively. We show how both types of grammar spectra can be collected by both LL and LR parsers, and how the JavaCC, ANTLR, and CUP parser generators can be modified and used to automate the collection of the grammar spectra. We also show how grammar spectra can be synthesized directly from test cases derived from a grammar, and how such synthetic spectra can be used to localize differences between a grammar and a black-box system under test. We first evaluate our approach over a large number of medium-sized single fault grammars, which we constructed by fault seeding from a common origin grammar. At the rule level, it ranks the rules containing the seeded faults within the top five rules in about 40%–70% of the cases, depending on the applied parsing technique, test suite, and ranking metric, and pinpoints them (i.e., correctly identifies them as unique most suspicious rule) in about 10%–30% of the cases, with significantly better results for the synthetic spectra. At the item level, our approach remains remarkably effective despite the larger number of possible locations, provided it is coupled with a simple tie-breaking strategy that prefers items with the right-most designated position over other items from the same rules in a tie. It typically ranks the seeded faults within the top five positions in about 30%–60% of the cases, and pinpoints them in about 15%–40% of the cases. This specialized item-level localization also significantly outperforms a simplistic extension of the rule-level localization, where all positions within a rule are given the same score. We further evaluate our approach over grammars that contain real faults. We show that an iterative method can be used to localize and manually remove one by one multiple faults in grammars submitted by students enrolled in various compiler engineering courses; in most iterations, the top-ranked rule already contains an error, and no error is ranked outside the top five ranked rules. We finally apply our approach to a large open-source SQLite grammar and show where this version deviates from the language accepted by the actual SQLite system.

In grammar-based testing, the test suites that drive the system under test are typically constructed from a given context-free grammar through a set of derivations that jointly satisfy some coverage criterion. In this paper, we describe and evaluate a new algorithm that instead constructs test suites from a set of valid paths that cover all edges in a labeled directed graph corresponding to an LR-automaton that accepts the language of the grammar. Vertices in this graph correspond to states in the LR-automaton; two vertices are connected by an edge iff the top of the LR-automaton's stack can change from one state to the other, either by shifting a terminal or non-terminal symbol (push edges), or by reducing with a grammar rule (pop edges). The algorithm constructs a unique reduction path for each pop edge in the graph. These reduction paths are recursively embedded into each other, and any unresolved non-terminal push edges are substituted by shortest derivations for the non-terminal symbol. The algorithm can work with different types of LR-automata, including LR(0)- and LR(1)-automata, and can successfully generate a test suite from an LR-graph even if the underlying LR-automaton construction leads to shift/reduce or reduce/reduce conflicts. The algorithm only constructs valid paths over the LR-graphs that correspond to sentences in the language and thus generates only positive tests. We therefore also describe mutations to the positive paths that are guaranteed to generate negative tests without needing any further verification by an oracle. Our algorithm is substantially more efficient than an earlier algorithm that explores LR-graphs with two consecutive breadth-first graph traversals and our experimental evaluation shows that it scales to large production-quality grammars. It is robust against random choices made to resolve ambiguity in the construction of the tests, while the code coverage of the different test suite variants is relatively uniform. Finally, our evaluation shows that the negative test suites constructed by path mutation identify more faults in a set of student grammars than those constructed by rule mutation.

Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL extension that improves the localization of a given base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that better localize the individual faults in the system. This allows it to identify and re-rank faults ranked too low by the base metric because they were masked by other program elements.

Dynamic program analysis tools such as Eraser, TaintCheck, or ThreadSanitizer abstract the contents of individual memory locations and store the abstraction results in a separate data structure called shadow memory. They then use this meta-information to efficiently implement the actual analyses. In this paper, we describe the implementation of an efficient symbolic shadow memory extension for the CBMC bounded model checker that can be accessed through an API, and sketch its use in the design of a new data race analyzer that is implemented by a code-to-code translation.

Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.

We describe the first approach to automatically repair bugs in context-free grammars: given a grammar that fails some tests in a given test suite, we iteratively and gradually transform the grammar until it passes all tests. Our core idea is to build on spectrum-based fault localization to identify promising repair sites (i.e., specific positions in rules), and to apply grammar patches at these sites whenever they satisfy explicitly formulated pre-conditions necessary to potentially improve the grammar.

The core of grammar-based test suite construction algorithms is a procedure to derive a set of specific phrases, which are then converted into sentences that can be fed into the system under test. This process includes several degrees of freedom and different implementations choose different but ultimately fixed solutions. We show that these fixed choices inherently bias the generated test suite.

We describe gtutr, an interactive feedback system designed to assist students in developing context-free grammars and corresponding ANTLR parsers. It intelligently controls students' access to a large test suite for the target language. After each submission, gtutr analyzes any failing tests and uses the Needleman-Wunsch sequence alignment algorithm over the tests' rule traces to identify and eliminate similar failing tests. This reduces the redundancy in the feedback

We report on our experience in using various grammar-based test suite generation methods to test 61 single-pass compilers that undergraduate students submitted for the practical project of a computer architecture course.

Test case generation from context-free grammars typically uses the grammar's production rules to directly construct words that cover specific sets of derivations. Here, we investigate test case generation by traversing graphs derived from the LR-automata corresponding to the grammars. We develop a new algorithm that generates positive test cases by covering all edges between pairs of directly connected states in a two-phase breadth-first path search. The algorithm iterates over all edges stemming from shift/reduce and reduce/reduce conflicts, using a technique similar to the stack duplication used in GLR parsing. We then extend our algorithm to generate negative (i.e., syntactically invalid) test cases, by applying different edge mutation operations during the extraction of test cases from paths.

Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleaving such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program's behaviours, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.

We describe and evaluate the first spectrum-based fault localization method aimed at finding faulty rules in a context-free grammar. It takes as input a test suite and a modified parser for the grammar that can collect grammar spectra, i.e., the sets of rules used in attempts to parse the individual test cases, and returns as output a ranked list of suspicious rules. We show how grammar spectra can be collected for both LL and LR parsers, and how the ANTLR and CUP parser generators can be modified and used to automate the collection of the grammar spectra. We evaluate our method over grammars with seeded faults as well as real world grammars and student grammars submitted in compiler engineering courses that contain real faults. The results show that our method ranks the seeded faults within the top five rules in more than half of the cases and can pinpoint them in 10%–40% of the cases. On average, it ranks the faults at around 25% of all rules, and better than 15% for a very large test suite. It also allowed us to identify deviations and faults in the real world and student grammars.

Grammar-based test case generation has focused almost exclusively on generating syntactically correct programs (i.e., positive tests) from a context-free reference grammar but a positive test suite cannot detect when the unit under test accepts words outside the language (i.e., false positives). Here, we investigate the converse problem and describe two mutation-based approaches for generating programs with guaranteed syntax errors (i.e., negative tests). % Word mutation systematically modifies positive tests by deleting, inserting, substituting, and transposing tokens in such a way that at least one impossible token pair emerges. % Rule mutation applies such operations to the symbols of the right-hand sides of productions in such a way that each derivation that uses the mutated rule yields a word outside the language.

Fault localisation, i.e. the identification of program locations that cause errors, takes significant effort and cost. We describe a fast model-based fault localisation algorithm that, given a test suite, uses symbolic execution methods to fully automatically identify a small subset of program locations where genuine program repairs exist. Our algorithm iterates over failing test cases and collects locations where an assignment change can repair exhibited faulty behaviour. Our main contribution is an improved search through the test suite, reducing the effort for the symbolic execution of the models and leading to speed-ups of more than two orders of magnitude over the previously published implementation by Griesmayer et al. We implemented our algorithm for C programs, using the KLEE symbolic execution engine, and demonstrate its effectiveness on the Siemens TCAS variants. Its performance is in line with recent alternative model-based fault localisation techniques, but narrows the location set further without rejecting any genuine repair locations where faults can be fixed by changing a single assignment. We also show how our tool can be used in an educational context to improve self-guided learning and accelerate assessment. We apply our algorithm to a large selection of actual student coursework submissions, providing precise localisation within a sub-second response time. We show this using small test suites, already provided in the coursework management system, and on expanded test suites, demonstrating the scalability of our approach. We also show compliance with test suites does not reliably grade a class of “almost-correct” submissions, which our tool highlights, as being close to the correct answer. Finally, we show an extension to our tool that extends our fast localisation results to a selection of student submissions that contain two faults.

ESBMC is a mature, permissively licensed open-source context-bounded model checker for the verification of single- and multi-threaded C programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions automatically. ESBMC provides C++ and Python APIs to access internal data structures, allowing inspection and extension at any stage of the verification process. We discuss improvements over previous versions of ESBMC, including the description of new front- and back-ends, IEEE floating-point support, and an improved k-induction algorithm. A demonstration is available at https://www.youtube.com/watch?v=YcJjXHlN1v8 .

Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program's interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.

Lazy sequentialization is one of the most effective approaches for the bounded verification of concurrent programs. Existing tools assume sequential consistency (SC), thus the feasibility of lazy sequentializations for weak memory models (WMMs) remains untested. Here, we describe the first lazy sequentialization approach for the total store order (TSO) and partial store order (PSO) memory models. We replace all shared memory accesses with operations on a shared memory abstraction (SMA), an abstract data type that encapsulates the semantics of the underlying WMM and implements it under the simpler SC model. We give efficient SMA implementations for TSO and PSO that are based on temporal circular doubly-linked lists, a new data structure that allows an efficient simulation of the store buffers. We show experimentally, both on the SV-COMP concurrency benchmarks and a real world instance, that this approach works well in combination with lazy sequentialization on top of bounded model checking.

Computer science instructors need to manage the rapid improvement of novice programmers through teaching, self-guided learning, and assessment. Appropriate feedback, both generic and personalised, is essential to facilitate student progress. Automated feedback tools can also accelerate the marking process and allow instructors to dedicate more time to other forms of tuition and students to progress more rapidly. Massive Open Online Courses rely on automated tools for both self-guided learning and assessment.

Open source code contributions contain a large amount of technical skill information about developers, which can help to identify suitable candidates for a particular development job and therefore impact the success of a development team. We develop CVExplorer as a tool to extract, visualize, and explore relevant technical skills data from GitHub, such as languages and libraries used. It allows non-technical users to filter and identify developers according to technical skills demonstrated across all of their open source contributions, in order to support more accurate candidate identification. We demonstrate the usefulness of CVExplorer by using it to recommend candidates for open positions in two companies.

Lazy-CSeq is a context-bounded verification tool for sequentially consistent C programs using POSIX threads. It first translates a multi-threaded C program into a bounded nondeterministic sequential C program that preserves bounded reachability for all round-robin schedules up to a given number of rounds. It then reuses existing high-performance bounded model checkers as sequential verification backends. Lazy-CSeq handles the full C language and the main parts of the POSIX thread API, such as dynamic thread creation and deletion, and synchronization via thread join, locks, and condition variables. It supports assertion checking and deadlock detection, and returns counterexamples in case of errors. Lazy-CSeq outperforms other concurrency verification tools and has won the concurrency category of the last two SV-COMP verification competitions.

Version control repositories contain a wealth of implicit information that can be used to answer many questions about a project's development process. However, this information is not directly accessible in the version control archives and must be extracted and visualized. This paper describes ConceptCloud, a flexible, interactive browser for SVN and Git repositories. The main novelty of our approach is the combination of an intuitive tag cloud visualization with an underlying concept lattice that provides a formal structure for navigation. ConceptCloud supports concurrent navigation in multiple linked but individually customizable tag clouds, which allows for multi-faceted repository browsing and for the construction of unique visualizations. We describe the mathematical foundations and implementation of our approach, and use ConceptCloud to quickly gain insight into the team structure and development process of two projects.

ConceptCloud is an interactive browser for SVN and Git repositories. Its main novelty is the combination of an intuitive tag cloud interface with an underlying concept lattice that provides a formal structure for navigation. This combination allows users to explore repositories serendipitously, without predefined search goals and along different navigation paths. ConceptCloud can derive different lattice types for a repository and supports concurrent navigation in multiple linked tag clouds that can each be individually customized, which allows multi-faceted repository explorations.

Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency preprocessing technique for automated sequential program verification tools. Our CSeq tool implements a novel sequentialization for C programs using pthreads, which extends the Lal/Reps sequentialization to support dynamic thread creation. CSeq now works with three different backend tools, CBMC, ESBMC, and LLBMC, and is competitive with state-of-the-art verification tools for concurrent programs.

Access control policies such as role-based access control (RBAC) enforce desirable security properties, in particular for Web-based applications with many different users. A fine-grained RBAC model gives the developers of such systems more customization and administrative power to control access to fine-granular elements such as individual cells of a table. However, the definition and deployment of such policies is not straightforward, and in many Web applications, they are hand-coded in the database or scattered throughout the application’s implementation, without taking advantage of underlying central elements, such as the data model or object types. This paper presents ΦRBAC, a fine-grained RBAC model for the Web application domain. ΦRBAC achieves separation of concerns for enforcing access to a range of objects with mixed-granularity levels. Moreover, it provides a unique testing mechanism that gives a guarantee to the developer about the correctness, completeness, and sufficiency of the defined ΦRBAC model, both internally and in the context of its target application. We use code generation techniques to compile the specification of a ΦRBAC model down to the existing tiers of an existing domain-specific Web programming language, WebDSL. We show the benefits of ΦRBAC on the development of a departmental Web site.

Propositional bounded model checking has been applied successfully to verify embedded software, but remains limited by increasing propositional formula sizes and the loss of high-level information during the translation preventing potential optimizations to reduce the state space to be explored. These limitations can be overcome by encoding high-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we propose the application of different background theories and SMT solvers to the verification of embedded software written in ANSI-C in order to improve scalability and precision in a completely automatic way. We have modified and extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions, and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded software applications from telecommunications, control systems, and medical devices. The experiments show that our ESBMC model checker can analyze larger problems than existing tools and substantially reduce the verification time.

The output of a code generator is assumed to be correct and not usually intended to be read or modified; yet programmers are often interested in this, e.g., to monitor a system property. Here, we consider code customization for a family of code generators associated with big-step executable modelling languages (e.g., statecharts). We introduce a customization language that allows us to express customization scenarios for the generated code independently of a specific big-step execution semantics. These customization scenarios are all different forms of runtime monitors, which lend themselves to a principled, uniform implementation for observation and code extension. A monitor is given in terms of the enabledness and execution of the transitions of a model and a reachability relation between two states of the execution of the model during a big step. For each monitor, we generate the aspect code that is incorporated into the output of a code generator to implement the monitor at the generated-code level. Thus, we provide means for code analysis through using the vocabulary of a model, rather than the detail of the generated code. Our technique not only requires the code generators to reveal only limited information about their code generation mechanisms, but also keeps the structure of the generated code intact. We demonstrate how various useful properties of a model, or a language, can be checked using our monitors.

We describe and evaluate three approaches to model check multi-threaded software with shared variables and locks using bounded model checking based on Satisfiability Modulo Theories (SMT) and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the SMT solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we bound the number of context switches allowed among threads in order to reduce the number of interleavings explored. We implemented these approaches in ESBMC, our SMT-based bounded model checker for ANSI-C programs. Our experiments show that ESBMC can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that use iterative context-bounding algorithms or counter-example guided abstraction refinement.

Manually implementing equals (for object comparisons) and hashCode (for object hashing) methods in large software projects is tedious and error-prone. This is due to many special cases, such as field shadowing, comparison between different types, or cyclic object graphs. Here, we present JEqualityGen, a source code generator that automatically derives implementations of these methods.

Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding word-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we investigate the application of different SMT solvers to the verification of embedded software written in ANSI-C. We have extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded software applications from telecommunications, control systems, and medical devices. The experiments show that our approach can analyze larger problems and substantially reduce the verification time.

Automated code generators are increasingly used in safety-critical applications, but since they are typically not qualified, the generated code must still be fully tested, reviewed, and certified. For mathematical and engineering software this requires reviewers to trace subtle details of textbook formulas and algorithms to the code, and to match requirements (e.g., physical units or coordinate frames) not represented explicitly in models or code. We support these tasks by using the AutoCert verification system to identify and verify mathematical concepts in the code, recovering verified traceability links between concepts, code, and verification conditions. We then exploit these links to construct a natural language report that provides a high-level structured argument explaining where the code uses specified assumptions and why and how it complies with the requirements. We have applied our approach to generate review documents for several sub-systems of NASA's Project Constellation.

We present a new, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over- and underflow, including mechanical transformation of program correctness proofs.

Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations.

Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e., pre- and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains difficult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator).Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property-specific abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding definitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.

Automated code generation offers many advantages over manual software development but treating generators as trusted black boxes raise problems for certification. Traditional process-oriented approaches to certification thus require that the generator be verified to the same level of assurance as the generated code, but this is infeasible for realistic generators. However, generators can be extended to support an evidence-based approach to certification. By careful design of the trusted kernel, assurance of the generator itself is not required. In this paper, we describe several related extensions to two in-house code generators to provide two forms of evidence along with the code: safety proofs and safety explanations. We also describe how additionally provided links are used to trace between the code and the safety artifacts.

Automated code generation is an enabling technology for model-based software development and promises many benefits, including higher quality and reduced turn-around times. However, the key to realizing these benefits is generator correctness: nothing is gained from replacing manual coding errors with automatic coding errors. In this paper, we describe an alternative technique that uses a generic post-generation annotation inference algorithm. We exploit both the highly idiomatic structure of automatically generated code and the restriction to specific safety properties. Since generated code only constitutes a limited subset of all possible programs, the new "eureka" insights required in general remain rare in our case. Since safety properties are simpler than full functional correctness, the required annotations are also simpler and more regular. We can thus use patterns to describe all code constructs that require annotations and templates to describe the required annotations. We use techniques similar to aspect-oriented programming to add the annotations to the generated code: the patterns correspond to (static) point-cut descriptors, while the introduced annotations correspond to advice. The annotation inference algorithm can run completely separately from the generator and is generic with respect to the safety property, although we use initialization safety as running example here. It has been implemented and applied to certify initialization safety for code generated by Auto-Bayes and AutoFilter

The goal of this workshop is to explore new technologies, underlying principles, and general methodologies for supporting software certificate management. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, which contain all the information necessary for an independent assessment of the demonstrated properties. Software certificates support a product-oriented assurance approach, combining different techniques and forms of evidence (e.g., fault trees, "sign-offs", safety cases, formal proofs, ...) and linking them to the details of the underlying software. A software certificate management system provides the infrastructure to create, maintain, and analyze software certificates. It combines functionalities of a database (e.g., storing and retrieving certificates) and a make-tool (e.g., incremental re-certification). It can also maintain links between system artifacts (e.g., design documents, engineering data sets, or programs) and different varieties of certificates, check the validity of certificates, provide access to explicit audit trails, enable browsing of certification histories, and enforce system-wide certification and release policies. It can at any time provide current information about the certification status of each component in the system, check whether certificates have been audited, compute which certificates remain valid after a system modification, or even automatically start an incremental recertification.

This paper presents a new methodology for automatic knowledge driven data mining based on the theory of Mercer Kernels, which are highly nonlinear symmetric positive definite mappings from the original image space to a very high, possibly infinite dimensional feature space. We describe a new method called Mixture Density Mercer Kernels (MDMK) to learn kernel function directly from data, rather than using pre-defined kernels. These data adaptive kernels can encode prior knowledge in the kernel using a Bayesian formulation, thus allowing for physical information to be encoded in the model. Specifically, we demonstrate the use of the algorithm in situations with extremely small samples of data. We compare the results with existing algorithms on data from the Sloan Digital Sky Survey (SDSS) and demonstrate the method's superior performance against standard methods. The results show that the Mixture Density Mercer Kernel described here outperforms tree-based classification in distinguishing high-redshift galaxies from low-redshift galaxies by approximately 16% on test data, bagged trees by approximately 7%, and bagged trees built on a much larger sample of data by approximately 2%. The code for these experiments has been generated with the AutoBayes tool, which automatically generates efficient and documented C/C++ code from abstract statistical model specifications. The core of the system is a schema library which contains templates for learning and knowledge discovery algorithms like different versions of EM, or numeric optimization methods like conjugate gradient methods. The template instantiation is supported by symbolic-algebraic computations, which allows AutoBayes to find closed-form solutions and, where possible, to integrate them into the code.

We take a typical scientific data analysis task, the analysis of planetary nebulae images taken by the Hubble Space Telescope, and describe how program synthesis can be used to generate the necessary analysis programs from high-level models. We describe the AutoBayes synthesis system, discuss its fully declarative specification language, and present the automatic program derivation starting with the scientists' original analysis.

Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability theory and numerical analysis, are well-founded but difficult to implement: the development of a statistical data analysis program for any given application is time-consuming and requires substantial knowledge and experience in several areas. In this paper, we describe A UTO B AYES , a program synthesis system for the generation of data analysis programs from statistical models. A statistical model specifies the properties for each problem variable (i.e. observation or parameter) and its dependencies in the form of a probability distribution. It is a fully declarative problem description, similar in spirit to a set of differential equations. From such a model, A UTO B AYES generates optimized and fully commented C/C++ code which can be linked dynamically into the Matlab and Octave environments. Code is produced by a schema-guided deductive synthesis process. A schema consists of a code template and applicability constraints which are checked against the model during synthesis using theorem proving technology. A UTO B AYES augments schema-guided synthesis by symbolic-algebraic computation and can thus derive closed form solutions for many problems. It is well-suited for tasks like estimating best-fitting model parameters for the given data. Here, we describe A UTO B AYES 's system architecture, in particular the schema-guided synthesis kernel. Its capabilities are illustrated by a number of advanced textbook examples and benchmarks.

Machine learning has reached a point where many probabilistic meth- ods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different instances of the EM algorithm. This enables the systematic derivation of algorithms cus- tomized for different models. Here, we describe the AUTO BAYES sys- tem which takes a high-level statistical model specification, uses power- ful symbolic techniques based on schema-based program synthesis and computer algebra to derive an efficient specialized algorithm for learning that model, and generates executable code implementing that algorithm. This capability is far beyond that of code collections such as Matlab tool- boxes or even tools for model-independent optimization such as BUGS for Gibbs sampling: complex new algorithms can be generated with- out new programming, algorithms can be highly specialized and tightly crafted for the exact structure of the model and data, and efficient and commented code can be generated for different languages or systems. We present automatically-derived algorithms ranging from closed-form solutions of Bayesian textbook problems to recently-proposed EM algo- rithms for clustering, regression, and a multinomial form of PCA. 1 Automatic Derivation of Statistical Algorithms Overview. We describe a symbolic program synthesis system which works as a “statistical algorithm compiler:” it compiles a statistical model specification into a custom algorithm design and from that further down into a working program implementing the algorithm design. This system, AUTOBAYES, can be loosely thought of as “part theorem prover, part Mathematica, part learning textbook, and part Numerical Recipes.” It provides much more flexibility than a fixed code repository such as a Matlab toolbox, and allows the creation of efficient algorithms which have never before been implemented, or even written down. AUTOBAYES is intended to automate the more routine application of complex methods in novel contexts. For example, recent multinomial extensions to PCA [2, 4] can be derived in this way.
The algorithm design problem. Given a dataset and a task, creating a learning method can be characterized by two main questions: 1. What is the model? 2. What algorithm will optimize the model parameters? The statistical algorithm (i.e., a parameter optimization algorithm for the statistical model) can then be implemented manually. The system in this paper answers the algorithm question given that the user has chosen a model for the data,and continues through to implementation. Performing this task at the state-of-the-art level requires an intertwined meld of probability theory, computational mathematics, and software engineering. However, a number of factors unite to allow us to solve the algorithm design problem computationally: 1. The existence of fundamental building blocks (e.g., standardized probability distributions, standard optimization procedures, and generic data structures). 2. The existence of common representations (i.e., graphical models [3, 13] and program schemas). 3. The formalization of schema applicability constraints as guards.1 The challenges of algorithm design. The design problem has an inherently combinatorial nature, since subparts of a function may be optimized recursively and in different ways. It also involves the use of new data structures or approximations to gain performance. As the research in statistical algorithms advances, its creative focus should move beyond the ultimately mechanical aspects and towards extending the abstract applicability of already existing schemas (algorithmic principles like EM), improving schemas in ways that gener- alize across anything they can be applied to, and inventing radically new schemas. 2 Combining Schema-based Synthesis and Bayesian Networks with 0 < n_points; 1 model mog as ’Mixture of Gaussians’; with 0 < nclasses with nclasses << n_points; with 1 = sum(I := 1..n_classes, phi(I)); 7 double phi(1..nclasses) as ’weights’ 8 9 double mu(1..nclasses); 9 double sigma(1..n_classes); 2 const int npoints as ’nr. of data points’ 3 4 const int nclasses := 3 as ’nr. classes’ 5 6 Statistical Models. Externally, AUTOBAYES has the look and feel of a compiler. Users specify their model of interest in a high-level specification language (as opposed to a program- ming language). The figure shows the specification of the mixture of Gaus- sians example used throughout this paper.2 Note the constraint that the sum of the class probabilities must equal one (line 8) along with others (lines 3 and 5) that make optimization of the model well-defined. Also note the ability to specify assumptions of the kind in line 6, which may be used by some algorithms. The last line specifies the goal 10 int c(1..npoints) as ’class labels’; 11 c ˜ disc(vec(I := 1..nclasses, phi(I))); 12 data double x(1..n_points) as ’data’; 13 x(I) ˜ gauss(mu(c(I)), sigma(c(I))); 14 max pr(x| phi,mu,sigma
) wrt phi,mu,sigma
;  inference task: maximize the conditional probability pr rameters 

Deductive retrieval and deductive synthesis are two conceptually closely related software development methods which apply theorem proving techniques to support the construction of correct programs. In this paper, we describe an integration of both methods which combines their complementary benefits and alleviates some of their drawbacks. The core of our integration is an algorithm which automatically extracts queries from the synthesis proof state and submits them to a specialized retrieval system. Retrieved components are then used to close open subgoals in the proof. We use a higher-order framework for synthesis in which higher-order meta-variables are used to represent program fragments still to be synthesized. Hence, the introduction of a new meta-variable is an attempt to synthesize a new fragment and so highlights a possible reuse step. This observation allows us to invoke retrieval only after a substantial change rather than at every proof step and prevents overloading the retrieval mechanism. Our integration raises the granularity level of synthesis by avoiding a substantial number of proof steps. It also provides a framework for adapting "near-miss" components in the case that an exact match cannot be retrieved.

Code synthesis is routinely used in industry to generate GUIs, form filling applications, and database support code and is even used with COBOL. In this paper we consider the question of whether code synthesis could also be applied to the data mining phase of knowledge discovery. We view this as a rapid prototyping method. Rapid prototyping of statistical data analysis algorithms would allow experienced analysts to experiment with different statistical models before choosing one, but without requiring prohibitively expensive programming efforts. It would also smooth the steep learning curve often faced by novice users of data mining tools and libraries. Finally, it would accelerate dissemination of essential research results and the development of applications. In this paper, we present a framework and the basic software for the automated synthesis of data analysis programs. We use a specification language that generalizes Bayesian networks, a popular notation used in many communities...

Specification-based retrieval provides exact content-oriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any deduction into an off-line indexing phase. In this paper, we show how match relations are used to build an appropriate index and how formal concept analysis is used to build a suitable navigation structure. This structure has the single-focus property (i.e. any sensible subset of a library is represented by a single node) and supports attribute-based (via explicit component properties) and object-based (via implicit component similarities) navigation styles. It thus combines the exact semantics of formal methods with the interactive navigation possibilities of informal methods. Experiments show that current theorem provers can solve enough of the emerging proof problems to make browsing feasible. The navigation structure also indicates situations where additional abstractions are required to build a better index and thus helps to understand and to re-engineer component libraries.

Deduction-based software component retrieval uses pre- and postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple but the vast number of arising proof tasks makes a practical implementation very hard. We thus pass the components through a chain of filters of increasing deductive power. In this chain, rejection filters based on signature matching and model checking techniques are used to rule out non-matches as early as possible and to prevent the subsequent ATP from "drowning". Hence, intermediate results of reasonable precision are available at (almost) any time of the retrieval process. The final ATP step then works as a confirmation filter to lift the precision of the answer set. We implemented a chain which runs fully automatically and uses SETHEO for model checking and the automated prover SETHEO as confirmation filter. We evaluated the system over a medium-sized collection of components. The results encourage our approach.

Abstract A large number of scanner generators have been developed. Since they are restricted to the longest‐match rule, they are unsuitable for an incremental environment. We present the ALADIN system, which is able to deliver more than a single token if required. Thus, an ambiguity may be passed to the calling instance. Beyond this ‘incremental feature’, ALADIN is a well‐structured and easy‐to‐understand language. In contrast to existing systems, the desired behaviour of the generated scanners is completely specified explicitly. Thus, the specifications are more abstract than in other systems. A prototype implementation has shown that ALADIN‐generated scanners have about the same performance as those generated by Lex.