Explore Projects

<p>SPF’s constraint interface needs to be restructured. The current implementation doesn’t allow for the easy addition of new solvers and could be optimized further. In order to do so, I propose the creation of a new hybrid list-tree data structure for the constraints of a path, roughly similar to that of the Abstract Syntax Tree utilized by the GREEN framework with the help of the visitor pattern. With this sort of data structure, SPF’s key backtracking features that allow for symbolic execution would remain intact, while the design of the constraint library would gain a level of abstraction that is not currently implemented in the code.</p>

<p>JPF-CORE currently builds and runs on Java 8. The main objective of this project is to get it up and running with Java 9, leveraging its new features like the modularity, strong encapsulation, while also handling the deprecates and removes. There are also other new enhancements like multi-release JAR files which is useful in supporting one or two major versions, in addition to just Java 9.</p>

<p>My projekt goal is to extend PSYCO by a symbolic search algorithm to generate a termination criteria for the learning phase and to enable PSYCO to check properties on reactive systems.</p> <p>The current JPF-PSYCO extension combines active automata learning and dynamic symbolic execution to generate interfaces of reactive components. Further in the accompanying theoretical work of Giannakopoulou et al.[1] is shown, that this interfaces are k-full, in case they are safe, permissive, and tight for all method sequences of length up to k, k ϵ ℕ. The evaluation part of the current PSYCO implementation shows that the choice of k heavily influences the runtime behavior of PSYCO. Further it is argued, that it is possible to choose k to a relative small value after a manual analysis of the source code. During my project I will implement a symbolic search on the symbolic transition system produced by JDART to generate possible good choices for k in an automated manner. Apart of the choice of k the symbolic search output can also be used to prove invariants on the analyzed components, e.g., the absence of assertion violations.</p>

<p>Extending jpf-nas tool.</p>

<p>Symbolic execution is a powerful analysis to systematically check assertions in programs. However, the already notorious scalability problem of symbolic execution is exacerbated by assertions. In our previous studies, we have introduced parallelism to check assertions with Symbolic Pathfinder (SPF) either with static analysis or dynamic analysis. In this work, we propose to combine static and dynamic analyses for parallel analysis to achieve better scalability, to further reduce the cost of symbolic execution using compositional and incremental assertion checking with SPF when the code or assertions are changed.</p>

<p>The state of art of program repair for heap manipulating program has focus on specific properties of bugs, like null pointer dereference. We try to fix programs with pre-condition and post-condition written in separation logic. Given a program, we first run JSF to collect its post-state(p) by symbolic execution with the given pre-condition. Then we check if p entails the given post-condition(p'). If not, a bug is detected. Our approach to program repair has two main components: abduction and repair specification inference. First, we propose to infer the missing information to establish the post-condition through abduction using an existing solver. In particular, we infer a constraint f such that p * f is satisfied and p * f |-&gt; p'. Secondly, based on abduction, we symbolically execute the input program with the abduction in a backward manner in order to construct repair specifications at every line of the input program. These repair specifications help to infer valid Hoare-style triples with fix candidates.</p>

<p>Veritesting, [1] is a promising technique that speeds up dynamic symbolic execution by multiple of factors [2]. In veritesting, expensive forking is minimized by statically analyzing and summarizing regions of code, which are then used during dynamic symbolic execution. During summer, I plan to a) extend veritesting to support test case generation for static re- gions, b) optimize instantiation of high-order regions based on benchmark results and c) work on a prototype to support static regions for 2-threaded programs.</p>

<p>Automated Program Repair (APR) has been showing a high capability recently of fixing software bugs automatically. Despite the recent advancements, there are only a few APR techniques specifically addressing regression errors. These techniques yet, however, have not fully exploited the information available in software evolution history, e.g., bug-inducing commits, etc, for repairing regression errors. Moreover, the techniques either work on a specific language (e.g., C language) or do not provide their implementations for public access.</p> <p>This project aims to empower automatic repair of regression errors for Java programs by implementing and extending recent interesting findings of regression errors, e.g., the correlation between bug-inducing and bug-fixing commits. We aim to build a system, namely LyFix, that enables users to fix Java regression bugs automatically by leveraging fix ingredients and specific repair operators learned from the software development history.</p>

<p>No one likes to arrive at the airport only to realize that their flight has been delayed. Departure Sensitive Arrival Spacing (DSAS) is a new concept developed at NASA Ames Research Center that has been shown to improve flight scheduling, enabling more departing planes to leave the runway. In order to fully evaluate the concept, it’s necessary to thoroughly test its impact on the workload of the human operators. Java Pathfinder can be used to check for just such a property.</p>

<p>This project will bring the JPF Inspector debugging tool up to date with the most recent version of JPF and Java, and it will add additional features, among which are a command-line interface, new commands and JPF introspection.</p>

<p>JDart is a tool for performing concolic execution on a Java program. The aim of concolic execution is to explore additional behavior in the program by generating input values which will result in a different path being taken through a program (or method). The result of concolic execution is a constraints tree, i.e., a tree with its inner nodes reflecting the decisions that were made during the execution of the program. The nodes on the trees are labeled as: OK if the method was regularly exited, ERROR if there was an exception, or DONT_KNOW if no valuation could be generated for the respective path.</p> <p>Currently, the constraints tree is represented only as a plain text file which makes identifying the nodes and the statuses of leaves extremely hard in such a simplistic representation. To provide a better user experience, I will develop a web interface to visualize the constraints trees generated by JDart. At a very basic level, a user will have an intuitive overview on the whole generated trees. At a later stage, I will enable interactive operations on the web interface, e.g. letting user select on which part of a tree JDart should focus on.</p>

<p>Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized by statically analyzing and summarizing regions of code, which are then used during dynamic symbolic execution. This technique was first introduced by the name of Veritesting[1] for c programs and recently implemented for Java programs in Java Ranger [2]. Both works report substantial benefits from merging of paths, with the latter winning SVComp’2020, a competition among Java verification and analysis tools.</p> <p>In this proposal, I plan to: 1) support test case generation for Java Ranger that would support branch coverage criteria, and 2) experiment the feasibility of path merging of threads by implementing a simulated thread interpreter and using Java Ranger to path merge thread interleavings.</p>

<p>Improving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a practical solution by combining the advantages of static symbolic execution (SSE) with those of dynamic symbolic execution (DSE). While Avgerinos et al. showed veritesting allows large-scale testing at the X86 binary level, it can also be applied to improve the performance of dynamic symbolic execution at the Java bytecode level. Symbolic PathFinder (SPF) performs symbolic execution for Java programs at the bytecode level. In this project, I plan to work on extending Symbolic PathFinder (SPF) to perform bounded static symbolic execution.</p>

<p>Symbolic PathFinder (SPF) has been very successful in testing and verifying Java bytecode programs with numeric inputs. However, its capability is very limited when coping with programs that have heap data structures. The underlying lazy initialization algorithm exhaustively enumerates all heap objects that can bind to the structured inputs accessed by the program. This enumeration may identify many invalid heap configurations that violate properties of the data structures in the heap, which leads to a huge amount of false alarms.</p> <p>We aim to tackle this problem by using separation logic, a well-known assertion language designed for reasoning about heap-manipulating programs. We will build a system, Java StarFinder (JSF), that enables users to describe properties of the data structures in the heap using separation logic. JSF is a symbolic execution engine, built on top of SPF, that generates path conditions (PCs) in the form of separation logic. These PCs are checked by a solver for satisfiability and test input generation. In addition, JSF can verify program correctness by collecting PCs satisfying some given preconditions and verifying if these PCs satisfy user-provided assertions.</p>

<p>Developers often perform recurrent tasks during the development process such as testing, managing external libraries, generating API documentation, and managing release artifacts. Build tools help to automate those error-prone and daunt tasks with scripts that abstract those tasks. This proposal aims to modernize the build workflow from the Java PathFinder (JPF) project by migrating from Ant to Gradle. Gradle is a general purpose build system and uses Groovy, a JVM language, to create flexible and highly customizable build workflows. To achieve this goal, my strategy is to have a working Gradle build coexisting with the current Ant script. Ant targets will migrate to Gradle tasks in an incremental and iterative process. By the end of the program, is expected to have the Gradle support fully integrated into the main repository.</p>

<p>Multithreaded programming is becoming a mainstream programming practice, while multithreaded programming is difficult and error prone. jpf-trace-server, an extension of Java PathFinder (JPF), can store and analyze traces. The error traces caused by deadlock can also be viewed in a new shell panel from jpf-shell.</p> <p>In this project, we will develop jpf-trace-server to trace the execution of the threads and to provide feedback to the programmer to help them fix the bugs. Inspired by previous work on visualization in JPF, we would like to show the thread interleavings as traces in a new panel of jpf-shell. We would like to show the source code in the panel along with the transition information. The users should be able to walk through each transition of a selected error trace and the corresponding source code where it is executed.</p>

<p>A engine to simplify Dynamic Partial Order Reduction in JPF as well as a tool to efficiently prove or disprove data race freedom in structured parallel programs that generalizes over input.</p>

<p>The goal of this project is to extend PocketSphinx so that it can calculate and provide alignments and acoustic scores for diphones similarly to how it already does for phonemes. This will help with learner analytics and adaptive instruction for pronunciation evaluation, assessment, and remediation, and can increase speech recognition accuracy and speech recognition system generality. Moreover, diphones may be helpful for new acoustic models, and can inform the construction of different kinds of language models.</p>

<p>CMUsphinx is a fast and flexible open source speech recognition toolkit. Currently it uses GMM acoustic models and it gives reasonable accuracy. This project is geared towards incorporating a state of the art MLP-HMM model into sphinx, substantially decreasing the error rates. A ResNet with MLPs instead of convolution networks will be trained and tested on TEDLIUM corpus.The aim is to achieve best-in-category accuracy in recognition of Ted talks.This project will bring CMUsphinx at par with other powerful speech toolkits like KALDI and will help Sphinx users worldwide get better accuracy in their ASR projects.</p>

<p>Traditionally, solid objects are represented as meshes: a set of vertices, edges, and faces. This interpretation of real-life objects into 3D space is sufficient for typically solid media such as teapots and chairs. However, this model faces many issues when used to represent dynamic materials such as smoke or clouds, which have innumerable and constant shifts in number and location of vertices, edges, and faces. These types of objects are typically classed and implemented separately as Volumes.</p> <p>Due to the nature of the materials involved, Volume rendering requires a different set of solutions in regards to data structuring, light sampling, and so on. Quickly becoming an industry standard, OpenVDB is a Volume rendering framework developed by Dreamworks that sees wide usage throughout the graphics industry such as in Pixar's RenderMan and Houdini. It is known for its efficiency in handling sparse data sets and its wide range of filters, transformation operators, compositing tools, and many other features for the creation and robust manipulation of Volumes. Its integration into Cycles will surely further Blender's usage in the 3D graphics scene.</p>

The aim of this project is to contribute to the open source community in synthetic image generation for MRI images. The advantages of Diffusion Models have been witnessed only recently in the field of Medical Imaging leaving scope for more exploration. For GSOC 2023, we intend to design models that can produce images conditioned on damage size, location, type etc. A probable use case for this project would be to perform inpainting to introduce a desired tumor or lesion. This would help in training large-scale data hungry models such as ViT to perform downstream tasks. And also help avoid training on multiple datasets sourced from different machines with varying parameters nor rely on Imagenet pre-trained models that suffer from change in domain distributional shift.

<p>Artificial Intelligence and Deep Learning nowadays are ever growing subjects. People who research AI, are experimenting with various intelligence models in order to discover a strong intelligence model which is equally capable with the unknown human model. Prototyping of such models (as large as they may be) needs to be as fast as possible, in order to examine exhaustively many novel ideas as fast as it can be done. For this we need to be able to use with ease as many resources as we have possible. As Theano is contributing to this attempt, current GPU technologies need to be supported extensively in a transient way through its framework. This can be achieved by including optimized operations from current NVidia frameworks, as well as optimizing or designing GPU code which resides in the framework’s backend. Furthermore, analysis and optimization of multi-gpu code, in addition with a consideration of a multi-node/gpu design, would prove themselves useful for this cause.</p>

<p>The aim of the project is to implement an automatic forecasting infrastructure for statsmodels similar to auto.arima()/ets() of the ‘ forecast’ package in R. The goals will be to use the existing models of statsmodels like SARIMAX and ES to build a forecasting method that would automatically detect the best model and forecast values based on that model.</p>