Hubbry Logo
Program analysisProgram analysisMain
Open search
Program analysis
Community hub
Program analysis
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Contribute something
Program analysis
Program analysis
Program analysis
View on Wikipedia
from Wikipedia
Part of a series on
Software development
Core activities
Paradigms and models
Methodologies and frameworks
Supporting disciplines
Practices
Tools
Standards and bodies of knowledge
Glossaries
Outlines

In computer science, program analysis[1] is the process of analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.

Program analysis can be performed without executing the program (static program analysis), during runtime (dynamic program analysis) or in a combination of both.

Static program analysis

[edit]
Main article: Static program analysis

In the context of program correctness, static analysis can discover vulnerabilities during the development phase of the program.[2] These vulnerabilities are easier to correct than the ones found during the testing phase since static analysis leads to the root of the vulnerability.

Due to many forms of static analysis being computationally undecidable, the mechanisms for performing it may not always terminate with the correct answer. This can result in either false negatives ("no problems found" when the code does in fact have issues) or false positives, or because they may never return an incorrect answer but may also never terminate. Despite these limitations, static analysis can still be valuable: the first type of mechanism might reduce the number of vulnerabilities, while the second can sometimes provide strong assurance of the absence of certain classes of vulnerabilities.

Incorrect optimizations are highly undesirable. So, in the context of program optimization, there are two main strategies to handle computationally undecidable analysis:

  1. An optimizer that is expected to complete in a relatively short amount of time, such as the optimizer in an optimizing compiler, may use a truncated version of an analysis that is guaranteed to complete in a finite amount of time, and guaranteed to only find correct optimizations.
  2. A third-party optimization tool may be implemented in such a way as to never produce an incorrect optimization, but also so that it can, in some situations, continue running indefinitely until it finds one (which may never happen). In this case, the developer using the tool would have to stop the tool and avoid running the tool on that piece of code again (or possibly modify the code to avoid tripping up the tool).

However, there is also a third strategy that is sometimes applicable for languages that are not completely specified, such as C. An optimizing compiler is at liberty to generate code that does anything at runtime – even crashes – if it encounters source code whose semantics are unspecified by the language standard in use.

Control-flow

[edit]
Main article: Control-flow analysis

The purpose of control-flow analysis is to obtain information about which functions can be called at various points during the execution of a program. The collected information is represented by a control-flow graph (CFG) where the nodes are instructions of the program and the edges represent the flow of control. By identifying code blocks and loops a CFG becomes a starting point for compiler-made optimizations.

Data-flow analysis

[edit]
Main article: Data-flow analysis

Data-flow analysis is a technique designed to gather information about the values at each point of the program and how they change over time. This technique is often used by compilers to optimize the code. One of the most well known examples of data-flow analysis is taint checking, which consists of considering all variables that contain user-supplied data – which is considered "tainted", i.e. insecure – and preventing those variables from being used until they have been sanitized. This technique is often used to prevent SQL injection attacks. Taint checking can be done statically or dynamically.

Abstract interpretation

[edit]
Main article: Abstract interpretation

Abstract interpretation allows the extraction of information about a possible execution of a program without actually executing the program. This information can be used by compilers to look for possible optimizations or for certifying a program against certain classes of bugs.

Type systems

[edit]
Main article: Type system

Type systems associate types to programs that fulfill certain requirements. Their purpose is to select a subset of programs of a language that are considered correct according to a property.

  • Type checking – verify whether the program is accepted by the type system.

Type checking is used in programming to limit how programming objects are used and what can they do. This is done by the compiler or interpreter. Type checking can also help prevent vulnerabilities by ensuring that a signed value isn't attributed to an unsigned variable. Type checking can be done statically (at compile time), dynamically (at runtime) or a combination of both.

Static type information (either inferred, or explicitly provided by type annotations in the source code) can also be used to do optimizations, such as replacing boxed arrays with unboxed arrays.

Effect systems

[edit]
Main article: Effect system

Effect systems are formal systems designed to represent the effects that executing a function or method can have. An effect codifies what is being done and with what it is being done – usually referred to as effect kind and effect region, respectively.[clarification needed]

Model checking

[edit]
Main article: Model checking

Model checking refers to strict, formal, and automated ways to check if a model (which in this context means a formal model of a piece of code, though in other contexts it can be a model of a piece of hardware) complies with a given specification. Due to the inherent finite-state nature of code, and both the specification and the code being convertible into logical formulae, it is possible to check if the system violates the specification using efficient algorithmic methods.

Dynamic program analysis

[edit]
Main article: Dynamic program analysis

Dynamic analysis can use runtime knowledge of the program to increase the precision of the analysis, while also providing runtime protection, but it can only analyze a single execution of the problem and might degrade the program’s performance due to the runtime checks.

Testing

[edit]
Main article: Software testing

Software should be tested to ensure its quality and that it performs as it is supposed to in a reliable manner, and that it won’t create conflicts with other software that may function alongside it. The tests are performed by executing the program with an input and evaluating its behavior and the produced output. Even if no security requirements are specified, additional security testing should be performed to ensure that an attacker can’t tamper with the software and steal information, disrupt the software’s normal operations, or use it as a pivot to attack its users.

Monitoring

[edit]

Program monitoring records and logs different kinds of information about the program such as resource usage, events, and interactions, so that it can be reviewed to find or pinpoint causes of abnormal behavior. Furthermore, it can be used to perform security audits. Automated monitoring of programs is sometimes referred to as runtime verification.

Program slicing

[edit]
Main article: Program slicing

For a given subset of a program’s behavior, program slicing consists of reducing the program to the minimum form that still produces the selected behavior. The reduced program is called a “slice” and is a faithful representation of the original program within the domain of the specified behavior subset. Generally, finding a slice is an unsolvable problem, but by specifying the target behavior subset by the values of a set of variables, it is possible to obtain approximate slices using a data-flow algorithm. These slices are usually used by developers during debugging to locate the source of errors.

See also

[edit]

References

[edit]

Further reading

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Program analysis

View on Grokipedia
from Grokipedia
Program analysis is a branch of focused on the automatic examination of computer programs to infer properties such as correctness, , , and behavior without necessarily executing the . It serves as a foundational technique for , enabling developers and engineers to detect bugs, optimize , and verify compliance with specifications in complex systems. The field addresses the inherent challenges of software complexity, where manual inspection becomes impractical, by providing scalable methods to analyze at various scales, from individual functions to large-scale distributed applications. At its core, program analysis divides into two primary categories: static analysis, which inspects source or compiled code without running it to extract facts like potential errors or dependencies, and dynamic analysis, which observes runtime behavior through execution traces or to capture actual program states. Static approaches, such as and , offer broad coverage but may produce false positives due to conservative approximations, while dynamic methods provide precise insights at the cost of requiring test inputs and potentially missing unexercised paths. These techniques underpin tools used in compilers for optimization, integrated development environments for real-time feedback, and security scanners for vulnerability detection. The theoretical foundations of program analysis trace back to early computability results, including Alan Turing's 1936 proof of the undecidability of the , which limits the precision of general analyses, and , establishing that non-trivial properties of program behavior are undecidable. Seminal advancements, like the formalization of by Patrick and Radhia Cousot in 1977, provided a rigorous framework for sound static analyses by mapping concrete program semantics to abstract domains. Today, the field continues to evolve with integrations of for improved precision and applications in emerging domains like and distributed systems.

Introduction

Definition and Goals

Program analysis is the systematic examination of software artifacts, such as , to infer properties about a program's behavior, structure, or performance without necessarily executing it. This field in employs automated techniques to approximate the dynamic behavior of programs, providing reliable insights into how software operates across possible executions. Analyses can occur at different representation levels, including for high-level semantic understanding, for intermediate portability in virtual machines, or for low-level efficiency in deployed systems. The primary goals of program analysis are to detect bugs by identifying potential defects like dereferences, verify program correctness against specifications, optimize code for better performance through techniques such as , ensure security by uncovering vulnerabilities like buffer overflows, and facilitate refactoring by revealing dependencies and structural insights. These objectives support broader , enabling developers to produce reliable and efficient systems. Key properties analyzed include code reachability to determine executable paths, to identify multiple references to the same location, and usage to assess demands on or . Program analysis integrates throughout the lifecycle, from initial design and implementation to testing, maintenance, and evolution, thereby reducing costs and enhancing reliability. Approaches encompass both static methods, which examine code without running it, and dynamic methods, which observe behavior during execution.

Historical Development

The origins of program analysis trace back to the late and early , during the development of early optimizing compilers for high-level programming languages. The I compiler, released by in 1957, incorporated rudimentary flow analysis techniques in its Sections 4 and 5 to determine the frequency of execution for different program paths, enabling basic optimizations such as and dead code removal through a simulation of . This marked one of the first systematic uses of program analysis for optimization, building on prior work in and integrated into the II system for the 7090 in 1961 by Vyssotsky and others. In the 1970s, program analysis advanced significantly with foundational work on data-flow frameworks. introduced a unified method for global in 1973, formalizing as iterative computations over lattices to propagate information across program control structures, proving convergence under certain conditions and enabling optimizations like constant propagation and reaching definitions. Concurrently, at developed key techniques for , including her 1970 framework for analyzing and transforming control-flow graphs, which influenced subsequent optimizations and earned her the 2006 for contributions to theory. The 1980s and 1990s saw the emergence of more formal and scalable approaches, expanding program analysis beyond optimization to verification. Patrick and Radhia Cousot formalized in 1977 as a unified lattice-based framework for approximating program semantics, allowing sound static analyses for properties like safety and termination by constructing fixpoints in abstract domains. Independently, in the early 1980s, Edmund Clarke and E. Allen Emerson developed for algorithmic verification of finite-state concurrent systems, while Joseph Sifakis and Jean-Pierre Queille advanced similar automata-based techniques; their combined innovations, recognized with the 2007 , enabled exhaustive exploration of state spaces for detecting errors in hardware and software. From the 2000s onward, program analysis integrated into modern toolchains and addressed security challenges, driven by and industry needs for scalability. Chris Lattner's framework, initiated in 2000 and detailed in 2004, provided a modular for lifelong program analysis using , facilitating optimizations and enabling widespread adoption in tools like for static analyses across languages. The 2014 vulnerability in spurred advancements in taint analysis, a dynamic and static technique for tracking untrusted data flows to prevent memory leaks and injections, with tools like demonstrating its role in detecting similar buffer over-reads through taint propagation from network inputs. This period also reflected a shift toward scalable in industry, such as in tools like KLEE (built on ), balancing precision with performance for verifying complex software. In the , program analysis has increasingly incorporated large language models to assist in tasks like static analysis, bug detection, and code understanding, further enhancing automation and precision in .

Classification of Program Analysis

Static versus Dynamic Analysis

Static analysis examines the source code or binary of a program without executing it, enabling reasoning about all possible execution behaviors to pursue exhaustive coverage of the program's state space. This approach is foundational in areas like optimization, where approximations of program semantics are computed to detect errors or optimize ahead of runtime. However, fundamental limits arise from undecidability, as demonstrates that non-trivial semantic properties of programs—such as whether a program computes a specific function—are inherently undecidable, necessitating over-approximations in static analyses that may include infeasible behaviors and lead to false positives. In contrast, dynamic analysis relies on executing the program, either in full or on selected inputs, to gather concrete observations of its runtime , yielding precise results for the paths actually traversed. This execution-based method excels in revealing real-world issues like performance bottlenecks or specific defects under given conditions but is inherently limited by incomplete path coverage, as the of possible execution paths—often termed path explosion—renders exhaustive testing impractical even for modest programs. The primary trade-offs between these approaches center on , precision, and . Sound static analyses guarantee detection of all errors (no false negatives) by over-approximating possible behaviors, though this conservatism reduces precision and increases false positives, while requiring substantial computational resources for . Dynamic analyses, conversely, offer high precision with no false positives for observed executions—since results stem directly from runs—but sacrifice due to potential misses in unexplored paths, though they are typically more efficient per test case. These complementary strengths have spurred hybrid techniques, such as concolic execution, which integrate execution with symbolic reasoning to balance coverage and precision without fully resolving the underlying challenges.

Soundness, Completeness, and Precision

In program analysis, soundness, completeness, and precision are fundamental properties that assess the reliability and accuracy of an analysis's results relative to the program's actual semantics, often formalized using denotational semantics where the concrete semantics denotes the set of all possible program behaviors. Soundness ensures that the analysis captures all true behaviors of the program, producing no false negatives; formally, if the concrete semantics of a program is the set of all reachable states or behaviors SS, a sound analysis yields an over-approximation S^\hat{S} such that S⊆S^S \subseteq \hat{S}. This property is crucial for verification tasks, as it guarantees that the absence of reported issues in the analysis implies no issues exist in reality. In the framework of abstract interpretation, soundness is established via a pair of abstraction function α\alpha and concretization function γ\gamma satisfying γ(α(x))⊒x\gamma(\alpha(x)) \sqsupseteq x for concrete values xx, ensuring the abstract domain correctly approximates the concrete one without omission. Completeness requires that the analysis results match the true behaviors exactly, with S^=S\hat{S} = S, eliminating both false negatives and false positives; in terms, this holds when α(γ(y))=y\alpha(\gamma(y)) = y for abstract values yy, meaning the approximation introduces no extraneous information. However, completeness is generally undecidable for nontrivial program properties due to the implications of the , which shows that determining exact semantic properties like termination or reachability is impossible in finite time for Turing-complete languages. Precision measures the tightness of the , quantifying how closely S^\hat{S} adheres to SS by minimizing spurious elements in over-approximations; for instance, it can be assessed via the width or of the abstract domain relative to the one, where narrower domains yield finer-grained results. Achieving high precision often involves trade-offs with , as more precise analyses require computationally intensive operations like narrowing to refine approximations, potentially increasing analysis time exponentially. These properties manifest differently across analysis types: static analyses typically employ over-approximation to ensure by including all possible behaviors (e.g., "may" analyses that report potentially reachable states), while dynamic analyses often use under-approximation, capturing only observed behaviors during execution (e.g., "must" analyses confirming definite properties in tested paths). This distinction aligns with the broader static-dynamic divide, where static methods prioritize exhaustive coverage at the cost of potential imprecision.

Static Program Analysis Techniques

Control-Flow Analysis

Control-flow analysis is a fundamental static technique in program analysis that models the possible execution paths of a program by constructing a (CFG). A CFG represents the program as a where nodes correspond to basic blocks—maximal sequences of straight-line code without branches or jumps—and edges indicate possible control transfers, such as conditional branches, unconditional jumps, loops, or procedure returns. This graph-based representation, pioneered in early optimization work, enables the identification of structured control elements like sequences, selections, and iterations without simulating execution. The construction of CFGs typically proceeds intraprocedurally, focusing on the control structure within a single function or procedure. Basic blocks are identified by partitioning the code at entry points, branch targets, and control-altering statements, with edges added based on the semantics of jumps, calls, and returns. For interprocedural analysis, which extends the CFG across procedure boundaries, additional edges connect call sites to entry nodes of callees and return sites to post-call nodes, often modeling the call graph to handle procedure interactions. However, precise interprocedural CFGs require approximations to avoid , such as treating calls as simple transfers or using call-string summaries for context sensitivity. Once constructed, CFGs facilitate computations of structural properties essential for further . Dominators are nodes through which every path from the entry must pass to reach a given node, computed efficiently using iterative algorithms that propagate dominance information forward from the entry; a simple, fast method iterates over a post-order traversal until fixed-point convergence, achieving near-linear time in practice. Post-dominators are defined analogously but backward from the exit node. These concepts underpin loop detection: natural loops are identified by back edges in a , where a back edge from node mm to nn defines a loop with header nn and body consisting of all nodes that can reach mm without passing through nn, enabling optimizations like . Introductory applications of CFGs involve solving basic data-flow problems to illustrate control . Reaching determines, for each program point, the set of variable assignments that may reach it along some path from the entry, formulated as a forward problem where definitions "gen" at assignment sites and are "kill"ed by subsequent redefinitions; solutions are computed via iterative over the CFG edges until fixed point. Similarly, live variables identifies variables used before their next definition along any path to the exit, a backward problem where uses "gen" at read sites and definitions "kill" liveness, aiding by revealing variable lifetimes. These computations highlight the CFG's role as a prerequisite for propagating abstract information in more advanced analyses. Despite their utility, CFGs face limitations in handling complex control features. Recursion introduces cycles in the interprocedural , potentially leading to infinite paths that require summarization or bounded call-string approximations to terminate . Exceptions and non-local transfers, such as those in languages like or C++, add irregular edges from throw sites to handlers, complicating graph construction and often necessitating separate exception-flow graphs or integrated modeling to capture all paths. Scalability issues arise in large codebases, where interprocedural CFGs can explode in size due to call-site multiplicity, though practical implementations mitigate this with on-demand construction and pointer analysis for call resolution, maintaining efficiency for programs up to millions of lines.

Data-Flow Analysis

Data-flow analysis is a framework for statically gathering information about the possible values of variables or expressions at various points in a program by propagating facts along paths in the . This technique enables the inference of program properties such as which definitions reach a use or which expressions are available, facilitating optimizations like and . Originating from early optimization efforts, it models data dependencies abstractly to avoid the undecidability of precise value tracking. The core framework employs a lattice structure to represent sets of facts at program points, where the lattice (L,⊓,⊔,⊥,⊤)(L, \sqcap, \sqcup, \bot, \top) defines the possible states, with ⊓\sqcap as the meet (join) operation for combining information at control-flow merges. Transfer functions f:L→Lf: L \to L describe how facts transform through statements and must be monotonic, preserving the partial order: if x⊑yx \sqsubseteq y, then f(x)⊑f(y)f(x) \sqsubseteq f(y). Analyses are solved via , computing the least fixed point of the data-flow equations over the lattice, which converges in finite steps due to the lattice's finiteness. The worklist implements this efficiently by maintaining a queue of nodes whose information needs updating, propagating changes until stabilization. Analyses are classified as forward or backward. Forward analyses, like reaching definitions, propagate information from program entry toward exit, while backward analyses, like available expressions, flow from exit toward entry. For a program point pp, the basic equations are: IN=\bigsqcapq∈pred(p)OUT\text{IN} = \bigsqcap_{q \in \text{pred}(p)} \text{OUT} OUT=fp(IN)\text{OUT} = f_p(\text{IN}) where fpf_p is the for pp, and \bigsqcap\bigsqcap is the meet over predecessors at join points. Classic problems illustrate the framework. Reaching definitions determines which variable assignments may reach a point, using a forward analysis with union (⊔=∪\sqcup = \cup) as the meet and sets of definitions as the lattice. The equations are: IN=⋃q∈pred(p)OUT\text{IN} = \bigcup_{q \in \text{pred}(p)} \text{OUT} OUT=gen∪(IN∖kill)\text{OUT} = \text{gen} \cup (\text{IN} \setminus \text{kill}) where gen\text{gen} are definitions generated at pp, and kill\text{kill} are those invalidated. Available expressions, a backward analysis for , tracks expressions computable at a point from entry, using (⊓=∩\sqcap = \cap) and analogous gen/kill sets in reverse. Constant propagation forwards constant values across assignments, employing a lattice of constants (e.g., ⊥\bot for unknown, specific values, or ⊤\top for non-constant), with transfer functions substituting constants where possible. Extensions address limitations in larger programs. Flow-insensitive analyses approximate by treating statement order loosely, often via fixed-point over all statements, to reduce at the cost of precision. Context-sensitive variants, crucial for interprocedural analysis, distinguish call sites by modeling calling contexts (e.g., via call strings or graph reachability), enabling precise propagation across procedures while maintaining polynomial-time solvability for distributive problems. These apply to by identifying unreachable or unused code through reaching definitions or live variables, removing it to reduce program size and execution time.

Abstract Interpretation

Abstract interpretation provides a general framework for the static analysis of programs by approximating their semantics in a way that ensures decidability and . Introduced by Patrick and Radhia Cousot, it formalizes program analysis as the interpretation of programs within abstract domains that over-approximate the concrete semantics of the program. This approach allows for the automatic determination of program properties by computing fixpoints in these abstract domains, which are typically lattices equipped with operations that mimic but simplify the concrete semantics. At the core of lies the theory of s between a domain ⟨C,⊑⟩\langle \mathcal{C}, \sqsubseteq \rangle representing the exact program semantics and an abstract domain ⟨A,⊑♯⟩\langle \mathcal{A}, \sqsubseteq^\sharp \rangle providing approximations. A is defined by a pair of monotonic functions α:C→A\alpha: \mathcal{C} \to \mathcal{A} () and γ:A→C\gamma: \mathcal{A} \to \mathcal{C} (concretization) such that for all c∈Cc \in \mathcal{C} and a∈Aa \in \mathcal{A}, α(c)⊑♯a\alpha(c) \sqsubseteq^\sharp a c⊑γ(a)c \sqsubseteq \gamma(a). is ensured because the abstract domain over-approximates the concrete one: γ(α(c))⊒c\gamma(\alpha(c)) \sqsupseteq c for all c∈Cc \in \mathcal{C}, meaning that any property proven in the abstract domain holds in the semantics, though the converse may not be true due to potential false positives. The process involves defining an abstract semantics ⟦⋅⟧♯\llbracket \cdot \rrbracket^\sharp that collects the effects of program statements in A\mathcal{A}, often by interpreting the program's in the abstract domain. For terminating computations, this is straightforward, but for loops and , termination is achieved using widening operators ∇:A×A→A\nabla: \mathcal{A} \times \mathcal{A} \to \mathcal{A}, which are monotonic functions satisfying x⊑♯∇(x,y)x \sqsubseteq^\sharp \nabla(x, y) and y⊑♯∇(x,y)y \sqsubseteq^\sharp \nabla(x, y), ensuring that iterative applications stabilize after finitely many steps to compute an over-approximation of the least fixpoint, often denoted Tω\mathsf{T}^\omega. Practical examples illustrate the framework's application. In interval analysis, the abstract domain consists of intervals [ℓ,u][\ell, u] for numerical variables, where α\alpha maps a set of concrete values to the tightest enclosing interval, and operations like addition are defined component-wise with appropriate handling for overflow or underflow. For instance, analyzing x=x+1x = x + 1 in a loop might yield an interval that widens to [−∞,+∞][-\infty, +\infty] after iterations, proving boundedness or detecting potential overflows conservatively. Sign analysis uses a simpler domain {−,0,+,⊤}\{ -, 0, +, \top \}, where ⊤\top represents unknown signs, and abstract operations propagate sign information through assignments and conditions, effectively handling non-determinism by merging possibilities into the least upper bound in the lattice. Non-determinism in inputs or control flow is managed by the join operation ⊔♯\sqcup^\sharp, which computes the least upper bound in A\mathcal{A}, ensuring the analysis remains sound by including all possible behaviors. The advantages of include its modular design, allowing analysts to define new abstract domains and operations tailored to specific properties without altering the underlying framework, and its deep connection to , where the concrete semantics serves as a semantic function that is lifted to the abstract level. This modularity facilitates the development of analyses for diverse properties, from numerical accuracy to resource usage. can be viewed as a special case of abstract interpretation using finite-height domains without explicit widening.

Type Systems

Type systems provide a static analysis mechanism in programming languages to assign types to variables, expressions, and functions, ensuring that operations are applied only to compatible data structures. This assignment is formally defined through typing rules, such as Γ⊢e:τ\Gamma \vdash e : \tau, where Γ\Gamma is a typing environment mapping variables to types, ee is an expression, and τ\tau is the inferred type of ee. These rules specify how types propagate through program constructs, for example, ensuring that the type of an application matches the function's parameter type. Seminal work on , particularly the Hindley-Milner algorithm, enables automatic derivation of principal types for polymorphic functions in languages like ML, achieving completeness for a decidable fragment of the with polymorphism. Static type checking uses these systems to detect type errors before program execution, preventing mismatches such as adding a string to an integer. Polymorphism enhances flexibility: parametric polymorphism allows functions like map to work uniformly across types without explicit instantiation, as in the Hindley-Milner system, while ad-hoc polymorphism, often via type classes or overloading, provides type-specific implementations, such as numeric operations on integers versus floats. Subtyping further refines this by permitting a type τ1\tau_1 to be safely substituted for τ2\tau_2 if τ1≤τ2\tau_1 \leq \tau_2, enabling structural compatibility in object-oriented languages, as formalized in structural subtyping rules. Advanced type systems extend these foundations to express richer program properties. Dependent types allow types to depend on program values, enabling specifications like array access within bounds (e.g., indexing an array of length nn only at positions from 0 to n−1n-1), as demonstrated in practical extensions to ML-like languages. Flow-sensitive refines by tracking type changes along control-flow paths, such as refining a variable's type after a conditional check, improving precision over flow-insensitive approximations. Type systems can be viewed as abstract interpretations over type lattices, specializing the general framework to safety properties. Despite their power, type systems face trade-offs between expressiveness and decidability; ensuring type checking remains computable limits their ability to verify arbitrary properties, such as catching all runtime errors like in general-purpose languages. For instance, full dependent types can encode undecidable propositions, necessitating restrictions for practical inference.

Model Checking

Model checking is an automated verification technique that exhaustively determines whether a finite-state model of a system satisfies a given specification, typically expressed in temporal logic. The models are commonly represented as Kripke structures, consisting of a set of states SS, a transition relation R⊆S×SR \subseteq S \times S, an initial state I⊆SI \subseteq S, and a labeling function L:S→2APL: S \to 2^{AP} that assigns subsets of atomic propositions APAP to each state. Specifications are formulated in logics such as Linear Temporal Logic (LTL) for linear-time properties or Computation Tree Logic (CTL) for branching-time properties; for instance, the CTL formula AG p→AF qAG \, p \rightarrow AF \, q asserts that whenever proposition pp holds invariantly from the initial state, proposition qq will eventually hold along some path. If the property fails, model checkers generate a counterexample trace—a finite path in the model violating the specification—to aid debugging. Core algorithms operate on automata-theoretic or symbolic representations to handle the verification. For LTL specifications, an automata-based approach constructs a Büchi automaton from the negation of the formula and checks the emptiness of the product automaton with the Kripke structure model. In software contexts, models are often expressed as Labelled Transition Systems (LTS), where transitions are labeled with actions, enabling the analysis of concurrent behaviors. Symbolic model checking, pioneered using Binary Decision Diagrams (BDDs), represents the state space implicitly to avoid explicit enumeration, as implemented in early tools like SMV for CTL formulas. To combat state explosion—the exponential growth in the number of states—techniques such as model minimization reduce equivalent states, while partial order reduction prunes the exploration by ignoring independent concurrent actions that do not affect the property. Originally developed for hardware verification in the early 1980s, has been extended to software systems, where finite-state abstractions of programs are checked against temporal properties. Seminal work by Clarke and Emerson introduced CTL model checking algorithms for branching-time logic in , demonstrating polynomial-time verification relative to the model size. Tools like SMV, first applied to circuit designs, influenced software extensions by providing counterexample-guided diagnostics. Scalability remains a primary challenge due to the state explosion in concurrent systems, often addressed through abstraction-refinement loops like Counterexample-Guided Refinement (CEGAR), which iteratively refines over-approximate abstract models upon discovering spurious counterexamples. This process ensures soundness by guaranteeing that valid counterexamples in the concrete model are preserved, though it requires careful predicate selection for effective refinement.

Dynamic Program Analysis Techniques

Testing

Testing is a fundamental dynamic program analysis technique that involves executing a program with selected inputs to observe its and verify whether it meets specified requirements. By running the software in a controlled environment, testing aims to uncover defects, ensure functionality, and assess reliability under various conditions. Unlike static analysis, which examines without execution, testing relies on actual runtime to detect issues such as crashes, incorrect outputs, or performance anomalies. This approach is essential in lifecycles, where it supports iterative validation from early stages to final deployment. Testing occurs at multiple levels to address different scopes of the system. focuses on individual components or functions in isolation, verifying their internal logic against expected behaviors. examines interactions between units, ensuring that combined modules function correctly without introducing new faults. evaluates the entire integrated application against overall requirements, often simulating real-world usage scenarios. These levels build progressively, with unit tests providing foundational confidence before broader integration and system validation. Testing strategies are broadly categorized as or , differing in their knowledge of internal structure. treats the program as a opaque entity, selecting inputs based on external specifications and checking outputs for correctness without examining code paths. In contrast, leverages knowledge of the program's internals to design tests that exercise specific structures, guided by coverage criteria such as statement coverage (executing every line), branch coverage (traversing all decision outcomes), or path coverage (exploring feasible execution paths). For safety-critical systems like , (MC/DC) is mandated, requiring each condition in a decision to independently affect the outcome, ensuring thorough fault detection in expressions. The testing process begins with test case generation, which can be manual, random, or model-based. Manual generation involves developers crafting inputs based on and requirements, allowing targeted exploration of edge cases but prone to human bias and incompleteness. Random testing automates input selection from input domains, often using feedback to refine sequences, as in tools like Randoop for , which generates unit tests by randomly composing method calls and pruning invalid ones. Model-based approaches derive tests from formal models of the system's behavior, such as state machines or UML diagrams, enabling systematic coverage of transitions and states. During execution, assertions embedded in code check invariants, while test oracles determine pass/fail by comparing actual outputs to expected results, often derived from specifications or historical data. Recent advancements include techniques for automated test generation, improving coverage and fault detection in complex systems as of 2024. Effectiveness of test suites is measured using metrics like and . Coverage metrics quantify how much of the code is exercised; for instance, branch coverage above 80% is often a threshold for adequate testing in industrial practices, though full path coverage is computationally infeasible for complex programs due to exponential paths. assesses suite quality by injecting small faults () into the code and verifying if tests detect them, with mutation scores indicating fault-detection capability; empirical studies have shown correlations between mutant detection and real fault revelation. Static path analysis can aid by identifying feasible paths for targeted test generation. Despite its strengths, testing has inherent limitations. It cannot prove the absence of bugs, as exhaustive testing is impractical for non-trivial programs, potentially missing defects in unexercised paths. The oracle problem exacerbates this for non-deterministic code, where outputs vary due to timing, concurrency, or external factors, making expected results hard to define without complete specifications. Thus, testing complements but does not replace other verification methods.

Runtime Monitoring

Runtime monitoring is a dynamic program analysis technique that observes and analyzes the execution of a program in real-time or post-execution to detect violations of specified properties, gather performance profiles, or identify anomalies during runtime. Unlike static analysis, which examines code without execution, runtime monitoring relies on actual program runs to collect data such as variable states, control flows, and system events, enabling the verification of behaviors that may be infeasible to predict statically. This approach is particularly valuable for systems where non-determinism or environmental interactions make exhaustive static prediction challenging. Key mechanisms for runtime monitoring include , which inserts probes or code snippets into the program to capture execution events, and event for recording traces that can be analyzed later. Probes can be added at compile-time, load-time, or runtime, often using techniques like binary tools (e.g., Pin or ) to avoid modifications. (AOP) provides a modular way to implement such by defining aspects that weave monitoring logic around specific join points, such as method calls or exceptions, without altering the core program structure. Event involves capturing sequences of events into traces, which are then processed for pattern matching or statistical analysis to infer system behavior. Applications of runtime monitoring span several areas, including invariant checking, where tools like dynamically infer and verify likely program invariants—such as range constraints or relational properties—by observing multiple executions and reporting those holding true across traces. For performance profiling, generates call graphs and execution time breakdowns by instrumenting functions to count calls and sample runtime, helping identify bottlenecks in large programs. Anomaly detection uses monitoring to flag deviations from expected patterns, such as unusual resource usage or security violations, often in real-time for immediate response. Modern applications include monitoring in AI and distributed systems, leveraging for anomaly prediction as of 2024. Runtime monitoring techniques distinguish between online analysis, which processes events as they occur to enable immediate feedback or enforcement (e.g., halting execution on violation), and offline analysis, which examines complete traces after execution for comprehensive post-mortem insights. Online monitoring suits time-sensitive applications like safety-critical systems, while offline allows deeper analysis without runtime constraints. Handling concurrency requires thread-safe monitors that synchronize access to shared state, often using atomic operations or lock-free data structures to avoid race conditions in multi-threaded environments. Significant challenges in runtime monitoring include minimizing overhead, as instrumentation can increase execution time by 10-50% or more depending on probe density and analysis complexity, prompting optimizations like selective sampling or hardware-assisted tracing. Non-determinism in traces, arising from concurrent scheduling, external inputs, or timing variations, complicates verification by producing variable execution paths, necessitating robust trace merging or probabilistic models to ensure reliable detection.

Program Slicing

Program slicing is a technique for reducing a program or its execution trace to a of statements that are relevant to a specific criterion, such as the value of a particular variable at a given program point. Introduced by in 1981, static program slicing operates on the source without executing it, producing a slice that includes all statements that may potentially affect the criterion across all possible executions. In contrast, dynamic program slicing, proposed by Bogdan Korel and Janusz Laski in 1988, focuses on a specific execution trace for given inputs, yielding a slice that captures only the statements that actually influence the criterion during that run. These approaches leverage program dependencies to isolate relevant computations, aiding in tasks like fault localization by eliminating irrelevant . The core algorithms for computing slices rely on dependence graphs that model control and flows in the program. A key representation is the program dependence graph (PDG), developed by Ferrante, Ottenstein, and Warren in 1987, which combines data dependences (how values flow between statements) and control dependences (how execution paths influence statement ) into a single directed graph. In backward slicing, the most common variant for , traversal starts from the slicing criterion and proceeds upstream through the dependence graph to include all predecessor statements that could impact it. Forward slicing, conversely, begins at a starting point and collects all downstream effects, useful for impact analysis. These graph-based methods ensure the slice preserves the semantics relevant to the criterion while removing extraneous parts. A slicing criterion typically specifies a variable vv and a program point (e.g., line ll), aiming to extract "all statements affecting vv at ll". For static slicing, algorithms like those using reaching definitions and live variables from data-flow analysis compute the slice by propagating dependencies across the entire control-flow graph. In dynamic slicing, computation involves an execution history or trace, where statements are filtered based on actual data flows during runtime; for instance, only executed paths contributing to the variable's value are retained, often using dynamic dependence graphs or post-execution marking of relevant instructions. This results in an executable subset that reproduces the criterion's behavior for the specific input. Program slicing finds primary applications in , where slices help isolate faults by focusing on code paths leading to erroneous values, as originally envisioned by Weiser. In , dynamic slices reduce test suites by selecting only relevant execution traces, improving efficiency without sacrificing coverage of critical behaviors. Additionally, slices enhance program comprehension by abstracting complex codebases to manageable views, facilitating maintenance and understanding of how changes propagate.

Example

Consider a simple program in :

1: input x 2: y = x + 1 3: if x > 0 then 4: z = y * 2 5: else 6: z = y 7: endif 8: output z

1: input x 2: y = x + 1 3: if x > 0 then 4: z = y * 2 5: else 6: z = y 7: endif 8: output z

A static backward slice for criterion ⟨z,8⟩\langle z, 8 \rangle includes lines 1–8, as all paths may affect zz. For input x=1x = 1, a dynamic slice might reduce to lines 1, 2, 3, 4, 7, 8, excluding the else branch.

Applications

Compiler Optimization

Compiler optimization leverages program analysis techniques to transform source code or intermediate representations into more efficient machine code, primarily aiming to minimize execution time, reduce code size, and lower resource usage while preserving program semantics. Static analyses, such as data-flow analysis, play a central role in identifying opportunities for transformations like dead code elimination, where unreachable or unused code is removed based on reaching definitions or liveness information. Constant folding evaluates and replaces constant expressions at compile time, simplifying computations that do not depend on runtime values. These intra-procedural optimizations rely on control-flow and data-flow frameworks to propagate information across basic blocks, enabling safe code removal or simplification without altering behavior. In the compiler pipeline, optimization occurs across multiple phases, starting in the front-end during semantic analysis to eliminate early redundancies, progressing to the middle-end for machine-independent transformations, and culminating in the back-end for architecture-specific adjustments. For instance, identifies computations within loops that yield the same value on every iteration and hoists them outside, reducing redundant operations; this is guided by data dependence analysis to ensure correctness. Register allocation in the back-end employs liveness analysis—a backward data-flow problem—to determine variable lifetimes, minimizing spills to and optimizing register usage for faster execution. Interprocedural analyses extend these to whole programs, constructing call graphs to enable inlining, where small or frequently called functions are merged into callers, eliminating call overhead and exposing further optimizations. Advanced optimizations like transform scalar loops into vector instructions for SIMD architectures, requiring precise dependence analysis to detect absence of data dependencies between loop iterations. This involves testing for flow, anti-, and output dependencies using techniques such as Banerjee's inequalities, which bound possible dependence distances to confirm parallelizability. In just-in-time () compilers, complements static methods by profiling execution at runtime to identify hot paths and apply targeted optimizations, such as speculative inlining based on observed call frequencies. For example, implementations use counter-based profiling to reorder code layout or specialize hot methods, adapting to actual workloads. These optimizations yield measurable benefits, with studies showing average speedups of 11% to 33% across GPU architectures through refined phase ordering, alongside code size reductions of up to 50% in selective sequences on large software packages. However, they introduce trade-offs, as aggressive analyses increase compilation time—sometimes by factors of 2-5—and may complicate debugging due to transformed code structures. Overall, the integration of static and dynamic analyses in modern compilers, such as and GCC, balances these factors to achieve substantial performance gains in production workloads.

Software Verification and Debugging

Software verification and debugging leverage program analysis techniques to ensure correctness and identify defects during software development. These methods systematically examine code or its execution to prove properties like safety invariants or locate faults, reducing reliance on manual inspection and enhancing reliability in complex systems. Formal verification approaches, such as , exhaustively explore state spaces to confirm that software satisfies specifications, while static analysis tools detect common errors like dereferences without running the program. In debugging, dynamic techniques trace data flows to pinpoint root causes, enabling developers to isolate issues efficiently. Integration of these analyses into development workflows further streamlines the process, from real-time feedback in editors to automated checks in build pipelines. In , formal methods like play a central role by automatically verifying that finite-state systems adhere to invariants expressed in . Pioneered in the , this technique constructs a model of the program and explores all possible executions to check for violations of safety or liveness properties, providing counterexamples if failures occur. For instance, it has been applied to concurrent systems to ensure deadlock freedom or . Complementing this, static checkers perform lightweight analyses on to identify potential defects; the FindBugs tool, for example, uses pattern-based detection to flag null pointer dereferences by tracking possible null values through control and data flows. These tools operate interprocedurally, propagating annotations to refine precision and reduce false positives, making them suitable for early-stage verification in large codebases. Debugging benefits from program analysis by narrowing the search space for faults. Program slicing, which extracts subsets of code relevant to a specific criterion like a variable or statement, aids fault localization by highlighting dependencies that could contribute to errors; techniques detailed elsewhere refine this for dynamic executions to rank suspicious statements. Dynamic taint tracking extends this by marking sensitive data at inputs and propagating taints through execution, revealing root causes such as unintended data influences leading to crashes or incorrect outputs. supports memory-related debugging by determining if objects allocated locally remain confined to a thread or method, helping identify leaks or issues without full execution traces. Tool integration embeds these analyses into everyday workflows for seamless verification and debugging. IDE plugins, such as SonarLint, provide on-the-fly static analysis within editors like or , flagging issues like null dereferences as developers write code and suggesting fixes based on rule sets. In pipelines, tools like automate verification by scanning builds for defects, enforcing quality gates before deployment and integrating with platforms such as Jenkins or GitHub Actions to halt faulty commits. For safety-critical domains, specialized integrations like LDRA's suite align analyses with standards, running coverage and static checks in automated workflows to verify compliance. A notable in illustrates the impact of program analysis under standards, which mandate rigorous verification for airborne software to achieve design assurance levels from A () to E (no effect). In developing flight control systems, employed structural coverage analysis to verify and detect unexercised paths, ensuring high coverage for DAL A while reducing manual review efforts. Similarly, a federal agency used Parasoft's unified testing platform, incorporating static analysis and unit verification, to comply with for embedded software, cutting testing time by automating defect detection and evidence generation. These applications demonstrate how analysis techniques mitigate risks in high-stakes environments, fostering safer software through proven, standards-aligned processes.

Security Analysis

Program analysis plays a crucial role in by identifying vulnerabilities that could lead to exploits, such as injection attacks or corruptions, through techniques that track flows and control transfers without executing the code. Static taint analysis, for instance, propagates labels on potentially malicious inputs to detect flaws like (SQLi), where untrusted reaches query construction points. In this approach, from external sources is marked as tainted and tracked through the program's control and flow graphs to identify unsafe uses, such as direct into SQL statements. A seminal implementation demonstrated its effectiveness in applications by achieving high precision in detecting SQLi alongside other taint-style vulnerabilities, reducing false positives through context-sensitive slicing. Dynamic symbolic execution complements static methods by exploring program paths with symbolic inputs during runtime, enabling the detection of buffer overflows where array bounds are exceeded due to unchecked inputs. This technique solves path constraints using satisfiability modulo theories (SMT) solvers to generate concrete inputs that trigger vulnerabilities, often uncovering deep bugs missed by traditional testing. For example, tools like KLEE apply dynamic symbolic execution to C programs, automatically generating tests that expose buffer overflows by systematically enumerating feasible execution paths and verifying assertions on memory accesses. Such analysis has proven effective in complex systems, achieving over 80% code coverage in benchmarks while identifying real-world memory errors. Key security properties enforced via program analysis include information flow control, which ensures non-interference by preventing sensitive data from influencing public outputs, and (CFI), which restricts indirect jumps to valid targets to thwart (ROP) attacks. Non-interference, formalized as a property where high-security inputs do not affect low-security observations, is verified through flow-sensitive analyses that model dependencies across program states. , in contrast, instruments binaries to check that control transfers align with a precomputed , mitigating ROP chains that repurpose existing code gadgets. The original CFI framework reduced exploit success rates to near zero in evaluated scenarios while incurring modest runtime overhead of 8-16%. Practical tools exemplify these techniques: Fortify performs static analysis to scan for taint leading to injections and other issues, supporting languages like and C# with customizable rulesets for enterprise security. , a dynamic framework, detects memory leaks and overflows at runtime by shadowing allocations and validating accesses, commonly used in C/C++ to prevent exploitation vectors like use-after-free. In web applications, static analysis detects (XSS) by modeling string operations and sink points like script insertions, with one approach identifying reflected XSS through value-flow tracking in code, achieving 92% precision on benchmarks. Post-2020, program analysis has increasingly addressed supply-chain attacks, as exemplified by the incident where was injected into software updates, compromising thousands of organizations. Analyses of such breaches employ binary instrumentation and dependency scanning to verify build integrity and detect tampered artifacts, emphasizing software bill of materials (SBOM) generation for tracking. Concurrently, AI-assisted methods, particularly large language models (LLMs) integrated with static analyzers, enhance detection by reasoning over code repositories to identify subtle patterns, outperforming traditional tools in recall for zero-day issues while reducing manual review efforts. techniques, detailed elsewhere, further support secure information flows in these contexts.

References

  1. https://dl.acm.org/doi/10.1145/3742900
  2. https://queue.acm.org/detail.cfm?id=3487021
  3. https://ics.uci.edu/~lopes/teaching/inf212W12/readings/Woegerer-progr-analysis.pdf
  4. https://dl.acm.org/doi/10.1145/512950.512973
  5. https://cmu-program-analysis.github.io/2023/lecture-slides/01-introduction.pdf
  6. https://dl.acm.org/doi/book/10.5555/1965094
  7. https://homes.cs.washington.edu/~mernst/pubs/program-analysis-book.pdf
  8. https://www.sciencedirect.com/topics/computer-science/program-analysis
  9. https://dl.acm.org/doi/pdf/10.1145/1500774.1500875
  10. https://www.cs.tufts.edu/~nr/cs257/archive/keith-cooper/survey.pdf
  11. https://www.ibm.com/history/frances-allen
  12. https://awards.acm.org/award_winners/allen_1012327
  13. https://dl.acm.org/doi/10.1145/1592761.1592781
  14. https://blog.trailofbits.com/2014/04/27/using-static-analysis-and-clang-to-find-heartbleed/
  15. https://www.sans.org/white-papers/35752/
  16. https://www.sciltp.com/journals/tai/articles/2505000685
  17. https://www.cs.nmsu.edu/~jcook/woda2003/papers/Ernst.pdf
  18. https://www.sciencedirect.com/science/article/abs/pii/S0920548919300066
  19. https://dl.acm.org/doi/10.1145/1064978.1065036
  20. https://dl.acm.org/doi/10.1145/567752.567778
  21. https://theory.stanford.edu/~aiken/publications/papers/cacm10.pdf
  22. https://drops.dagstuhl.de/opus/volltexte/2020/13226/pdf/OASIcs-Gabbrielli-4.pdf
  23. https://se421-fall2018.github.io/resources/readings/p1-allen.pdf
  24. https://dl.acm.org/doi/10.1145/800028.808479
  25. https://cs.au.dk/~amoeller/spa/spa.pdf
  26. https://www.cs.cmu.edu/~aldrich/courses/15-819O-13sp/resources/interprocedural.pdf
  27. https://www.cs.tufts.edu/~nr/cs257/archive/keith-cooper/dom14.pdf
  28. https://yanniss.github.io/doop-issta09prelim.pdf
  29. https://dl.acm.org/doi/10.1145/360018.360025
  30. https://dl.acm.org/doi/10.1145/512927.512945
  31. https://dl.acm.org/doi/10.1145/199448.199462
  32. https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml
  33. https://cs.nyu.edu/~pcousot/COUSOTpapers/JLP92.shtml
  34. https://cs.nyu.edu/~pcousot/publications.www/Cousot-Klaus-Havelund-Festschrift.pdf
  35. https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
  36. https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/milner-type-polymorphism.pdf
  37. https://people.eecs.berkeley.edu/~necula/Papers/DamasMilnerAlgoW.pdf
  38. https://dl.acm.org/doi/10.1145/582153.582176
  39. http://lucacardelli.name/papers/onunderstanding.a4.pdf
  40. http://lucacardelli.name/Papers/StructuralSubtyping.pdf
  41. https://www.cs.cmu.edu/~fp/papers/popl99.pdf
  42. https://theory.stanford.edu/~aiken/publications/papers/pldi02.pdf
  43. https://www.andrew.cmu.edu/user/liminjia/research/papers/popl10-lambda-eek.pdf
  44. https://courses.physics.illinois.edu/cs421/resources/cardelli.pdf
  45. https://www.cs.cmu.edu/~emc/15414-s14/lecture/ModelChecking.pdf
  46. https://www.cs.cmu.edu/~15414/s20/2018/lectures/17-ctl.pdf
  47. https://www.cs.cmu.edu/~flerda/publications/clarke07model.pdf
  48. https://www.cs.rice.edu/~vardi/papers/Verification-HB21.pdf
  49. http://convecs.inria.fr/doc/publications/Lang-Mateescu-12.pdf
  50. https://www.cs.colostate.edu/~france/CS614/Readings/Readings2011/Model-checking-Survey-a21-jhala.pdf
  51. https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf
  52. https://www.cs.cmu.edu/~nishants/trs/cmu-cs-07-110.pdf
  53. https://web.stanford.edu/class/cs357/cegar.pdf
  54. https://dl.acm.org/doi/10.1145/1297846.1297902
  55. https://dl.acm.org/doi/10.1145/267580.267590
  56. https://ieeexplore.ieee.org/document/6963470
  57. https://dl.acm.org/doi/fullHtml/10.1145/3452383.3452388
  58. https://dl.acm.org/doi/10.1145/3613905.3623774
  59. https://homes.cs.washington.edu/~mernst/pubs/mutation-effectiveness-fse2014.pdf
  60. https://dl.acm.org/doi/10.1145/567446.567468
  61. https://arxiv.org/abs/1708.07229
  62. https://ieeexplore.ieee.org/document/8342921/
  63. https://www.sciencedirect.com/science/article/pii/S1574013723000618
  64. https://dl.acm.org/doi/10.1145/2134243.2134246
  65. https://www.sciencedirect.com/science/article/pii/S016764230700161X
  66. https://dl.acm.org/doi/10.1145/872726.806987
  67. https://dl.acm.org/doi/10.1145/3652595.3660697
  68. https://www.um.edu.mt/library/oar/bitstream/123456789/23140/1/main.pdf
  69. https://link.springer.com/article/10.1007/s10703-019-00337-w
  70. https://dl.acm.org/doi/10.1145/3650212.3680400
  71. https://www.franktip.org/pubs/jpl1995.pdf
  72. https://dl.acm.org/doi/10.5555/800078.802557
  73. https://www.sciencedirect.com/science/article/pii/0020019088900543
  74. https://dl.acm.org/doi/10.1145/24039.24041
  75. https://dl.acm.org/doi/10.1145/800192.805690
  76. https://www.semanticscholar.org/paper/A-unified-approach-to-global-program-optimization-Kildall/d233d7d5a0ebbbf4d02dbb3d21a64b86863f06ca
  77. https://www.clear.rice.edu/comp512/Lectures/Papers/1971-allen-catalog.pdf
  78. https://www.cs.tufts.edu/comp/150IPL/papers/aycock03jit.pdf
  79. https://suif.stanford.edu/~jwhaley/papers/javagrande99.pdf
  80. https://www.research.ed.ac.uk/files/70048258/Machine_Learning_in_compiler_optimisation.pdf
  81. http://publish.illinois.edu/allvm-project/files/2022/01/bartell-dissertation-2021.pdf
  82. https://dl.acm.org/doi/10.1145/3446804.3446849
  83. https://dl.acm.org/doi/10.1145/5397.5399
  84. https://www.cs.tufts.edu/comp/150CMP/papers/pugh04findbugs.pdf
  85. https://www.cse.msu.edu/~cse870/Public/Homework/SS2003/HW5/p439-weiser.pdf
  86. https://www.ndss-symposium.org/wp-content/uploads/2017/09/Dynamic-Taint-Analysis-for-Automatic-Detection-Analysis-and-SignatureGeneration-of-Exploits-on-Commodity-Software-Dawn-Song.pdf
  87. https://faculty.cc.gatech.edu/~harrold/6340/cs6340_fall2009/Readings/choi99escape.pdf
  88. https://www.sonarsource.com/resources/library/static-code-analysis-using-sonarqube/
  89. https://ldra.com/capabilities/continuous-integration/
  90. https://www.rapitasystems.com/downloads/collins-aerospace-do-178c-code-coverage-analysis
  91. https://www.parasoft.com/resources/case-studies/federal-agency-fulfills-rigorous-do-178c-standard-with-unified-automated-testing-solution/
  92. https://www.usenix.org/event/sec05/tech/full_papers/livshits/livshits.pdf
  93. https://llvm.org/pubs/2008-12-OSDI-KLEE.pdf
  94. https://users.soe.ucsc.edu/~abadi/Papers/cfi-tissec-revised.pdf
  95. https://www.opentext.com/products/static-application-security-testing
  96. https://valgrind.org/
  97. https://dl.acm.org/doi/10.1145/1368088.1368112
  98. https://www.cisa.gov/news-events/cybersecurity-advisories/aa20-352a
  99. https://arxiv.org/abs/2405.15614
Add your contribution
Related Hubs
Contribute something
User Avatar
No comments yet.