相关论文: An Empirical Study of Path Feasibility Queries

In many practical application domains, the software is organized into a set of threads, whose activation is exclusive and controlled by a cooperative scheduling policy: threads execute, without any interruption, until they either terminate…

The recent advancements of Small Language Models (SLMs) have opened new possibilities for efficient code generation. SLMs offer lightweight and cost-effective alternatives to Large Language Models (LLMs), making them attractive for use in…

Satisfiability Modulo Theories (SMT) specifications often rely on quantifiers to remain concise and declarative. However, checking the satisfiability of such specifications directly can be inefficient. A common optimization is to ground the…

Providing safety guarantees for stochastic dynamical systems is a central problem in various fields, including control theory, machine learning, and robotics. Existing methods either employ Stochastic Barrier Functions (SBFs) or rely on…

Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free functions conforming to a specification given as a logical…

Empirical software engineering is concerned with the design and analysis of empirical studies that include software products, processes, and resources. Optimization is a form of data analytics in support of human decision-making.…

In recent years, quantum, quantum-inspired, and hybrid algorithms are increasingly showing promise for solving software engineering optimization problems. However, best-intended practices for conducting empirical studies have not yet well…

We present SEIF, a methodology that combines static analysis with symbolic execution to verify and explicate information flow paths in a hardware design. SEIF begins with a statically built model of the information flow through a design and…

Probabilistic graphical models have emerged as a powerful modeling tool for several real-world scenarios where one needs to reason under uncertainty. A graphical model's partition function is a central quantity of interest, and its…

Satisfiability Modulo Theories (SMT) solvers are integral to program analysis techniques like concolic and symbolic execution, where they help assess the satisfiability of logical formulae to explore execution paths of the program under…

Probabilistic software analysis aims at quantifying the probability of a target event occurring during the execution of a program processing uncertain incoming data or written itself using probabilistic programming constructs. Recent…

Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating satisfiability of S5…

String constraint solving, and the underlying theory of word equations, are highly interesting research topics both for practitioners and theoreticians working in the wide area of satisfiability modulo theories. As string constraint solving…

Finite State Machine is a popular modeling notation for various systems, especially software and electronic. Test paths can be automatically generated from the system model to test such systems using a suitable algorithm. This paper…

Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the main goal of symbolic…

The use of random sampling in decision-making and control has become popular with the ease of access to graphic processing units that can generate and calculate multiple random trajectories for real-time robotic applications. In contrast to…

Applying robust optimization often requires selecting an appropriate uncertainty set both in shape and size, a choice that directly affects the trade-off between average-case and worst-case performances. In practice, this calibration is…

While there has been some discussion on how Symbolic Computation could be used for AI there is little literature on applications in the other direction. However, recent results for quantifier elimination suggest that, given enough example…

Search-based software testing (SBST) is now a mature area, with numerous techniques developed to tackle the challenging task of software testing. SBST techniques have shown promising results and have been successfully applied in the…

In quantum software engineering (QSE), quantum software testing (QST) has attracted increasing attention as quantum software systems grow in scale and complexity. Since QST evaluates quantum programs through execution under designed test…