Software Analysis & Verification  |
| |
| NIST Report: The Economic Impacts Of Inadequate Infrastructure For Software Testing |
|
|
| Sustainable Computing Consortium |
|
|
| Model Checking |
|
|
| Model Checking Accomplishments And Opportunities |
|
|
| Ballista Project COTS Software Robustness Testing |
|
|
| Ballista Publications |
|
|
| Different Aspects Of Security Problems In Network Operating Systems |
|
|
| Robust Software - No More Excuses |
|
|
| Philip Koopman's Home Page Dependable Embedded Systems Research |
|
|
| SLAM Project Microsoft Research |
|
|
| Speeding Up Data Flow Analysis Using Flow-Insensitive Pointer Analysis |
|
|
| The SLAM Project: Debugging System Software Via Static Analysis |
|
|
| Automatically Validating Temporal Safety Properties of Interfaces |
|
|
| The SLAM Toolkit |
|
|
| Checking Temporal Properties Of Software With Boolean Programs |
|
|
| Boolean Programs: A Model And Process For Software Analysis |
|
|
| SLIC: A Specification Language For Interface Checking (Of C) |
|
|
| Bebop: A Path-Sensitive Interprocedural Dataflow Engine |
|
|
| Bebop: A Symbolic Model Checker For Boolean Programs |
|
|
| Polymorphic Predicate Abstraction |
|
|
| Automatic Predicate Abstraction Of C Programs |
|
|
| Tools And Algorithms For The Construction And Analysis Of Systems (Book) |
|
|
| Boolean And Cartesian Abstraction For Model Checking C Programs |
|
|
| Generating Abstract Explanations Of Spurious Counterexamples In C Programs |
|
|
| Relative Completeness Of Abstraction Refinement For Software Model Checking |
|
|
| Parameterized Verification Of Multithreaded Software Libraries |
|
|
| Specifying And Checking Properties Of Programs |
|
|
| BLAST Berkeley Lazy Abstraction Software Verification Tool |
|
|
| MOPED - A Model-Checker For Pushdown Systems |
|
|
| Bandera Project Finite-State Verification Techniques |
|
|
| The IBM Canvas Project |
|
|
| NASA Automated Software Engineering Group Verification & Validation |
|
|
| Alchemy Project |
|
|
| Model Checking At CMU |
|
|
| Center For High Assurance Computer Systems |
|
|
| LASER Laboratory Of Advanced Software Engineering Research |
|
|
| Gimpel Software |
|
|
| ESP Project Error Detection Via Scalable Program Analysis |
|
|
| Compaq Extended Static Check For Java (ESC/Java) |
|
|
| Meta-Level Compilation (MC Project) |
|
|
| MOPS Model Checking Programs For Security Properties |
|
|
| Open Source Quality |
|
|
| PALE - The Pointer Assertion Logic Engine |
|
|
| The MONA Project |
|
|
| PolySpace Next Generation Development Tools For Embedded Applications |
|
|
| Programatica: Integrating Programming, Properties, And Validation |
|
|
| Oxford Programming Tools Group |
|
|
| Prover Technology Proof Engine |
|
|
| Secure Software System (S3) Group |
|
|
| Semantic Designs: Automated Large-Scale Software System Analysis, Modification, Translation and Generation |
|
|
| CMU Specification And Verification Center (SVC) |
|
|
| Splint Annotation-Assisted Lightweight Static Checking |
|
|
| SRI Formal Methods And Dependable Systems |
|
|
| Improving Program Robustness via Static and Dynamic Analysis |
|
|
| TVLA 3-Valued Logic Analysis Engine |
|
|
| VAULT A Programming Language For Reliable Systems |
|
|
| VeriSoft A Tool For Systematic Software Testing |
|
|
| The VFiasco Project |
|
|
| Wisconsin Safety Analyzer |
|
|
Yahoda Verification Tools Database  |
|
|
| On-The-Fly, LTL Model Checking With SPIN |
|
|
| The Model Checking Kit |
|
|
| Model Checking Links |
|
|
| The 10th International SPIN Workshop On Model Checking |
|
|
| Modeling And Model-Checking |
|
|
| Planning As Model Checking Tutorial |
|
|
| Model Checking And Abstraction |
|
|
| Model Checking (Book) 2000 |
|
|
| Reactive Systems And Model Checking From Concept To Tool |
|
|
| Model Checking Publish-Subscribe Systems |
|
|
| The Rise Of Model Checking |
|
|
| Model Checking Electronic Commerce Protocols |
|
|
| Model Checking Operator Procedures |
|
|
| Model Checking: A Tutorial Overview |
|
|
| Infinite State Model Checking And Debugging |
|
|
| Univariate Stochastic ARIMA Model Checking |
|
|
| E-Process Design And Assurance Using Model Checking |
|
|
| Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis |
|
|
| Symbolic Model Checking |
|
|
| Fixed-Parameter Tractability, Definability, and Model-Checking |
|
|
| Using Model Checking To Debug Device Firmware |
|
|
| Towards TLA+ Model Checking |
|
|
| Model Checking The Transmit Master/Receive Slave (TMRS) Using Formalcheck |
|
|
| Applying Model Checking To Large Software Specifications |
|
|
| Compositional Model-Checking For Algol With Active Expressions |
|
|
| Designing A Controlled Language For Interactive Model Checking |
|
|
| Examples Of SAT Problems From Bounded Model Checking An Alpha Design |
|
|
| Verification, Model Checking And Abstract Interpretation |
|
|
| Model Checking For Abstract State Machines |
|
|
| Model Checking Infinite State Spaces |
|
|
| A Direct Symbolic Approach To Model Checking Pushdown Systems |
|
|
| Combining Symbolic And Partial Order Methods For Model Checking 1-Safe Petra Nets |
|
|
| Temporal Logic Model Checking of CSP: Tools And Techniques |
|
|
| Bounded Model Checking For Timed Automata |
|
|
| Refining Model Checking By Abstract Interpretation |
|
|
| Model Checking Java Programs Using Structural Heuristics |
|
|
| The Quest For Correct Systems: Model Checking Of Diagrams And Datatypes |
|
|
| SAT-Based Model Checking For Error Detection In Security Protocols |
|
|
| Model Checking With Multi-Valued Temporal Logics |
|
|
| Using Fixpoint Characterisations Of LTL For Bounded Model Checking |
|
|
| Performance And Reliability Model Checking And Model Construction |
|
|
| Bounded LTL Model Checking With Stable Models |
|
|
| Using Model Checking To Validate AI Planner Domain Models |
|
|
| A Logic of Belief and a Model Checking Algorithm for Security Protocols |
|
|
| Symbolic Model Checking for Self-Stabilizing Algorithms |
|
|
| Symbolic Model Checking Of Dual Transition Petri Nets |
|
|
| Using Model Checking To Generate Tests From Large Software Specification |
|
|
| An Approach To Compositional Model Checking |
|
|
| Transformation Verification Simulation (TVS) Publications |
|
|
| Partial Order Reduction Assisted Parallel Model-Checking |
|
|
| The Complexity of Model Checking in Modal Event Calculi with Quantifiers |
|
|
| Bounded Model Checking Using Satisfiability Solving |
|
|
| Model Checking Applications |
|
|
| Verification Via Model Checking |
|
|
| Deductive Model Checking |
|
|
| Model Checking Java Programs |
|
|
| Model Checking In Industry |
|
|
| Probabilistic Symbolic Model Checking |
|
|
| Symbolic Model Checking Of Biological Systems |
|
|
| Symbolic Model Checking In Coq |
|
|
| Model Checking For CTL |
|
|
| MCWEB - A Model-Checking Tool For Web Site Debugging |
|
|
| Model Checking The Composition Of Hypermedia Design Components |
|
|
| Using Model Checking to Analyze Network Vulnerabilities |
|
|
| CIP Model Checking Project |
|
|
| Model Checking Concurrent Java Software Using The Bandera Tool Set |
|
|
| Unified Assertion-Based Functional Verification - Model Checking, Simulation And Debugging |
|
|
| Stable Model Checking Made easy |
|
|
| Software Metrics And Static Analysis |
|
|
| NWG1: Static Analysis |
|
|
| Security And Safety Through Static Analysis |
|
|
| Static Analysis For Security And Safety (SASS) |
|
|
| Security Through Static Analysis |
|
|
| Static Analysis Of Large Programs: Some Experiences |
|
|
| Static Analysis With LDRA Testbed |
|
|
| Improving Security Using Extensible Lightweight Static Analysis |
|
|
| Linear Static Analysis |
|
|
| NISA II/ Linear Static Analysis |
|
|
| Validation Of Critical Software By Static Analysis And abstract Testing |
|
|
| Static Analysis Tools |
|
|
| Static Analysis For A Software Transformation Tool |
|
|
| Java Static Analysis |
|
|
| Static Analysis For Dynamic XML |
|
|
| Intrusion Detection Via Static Analysis |
|
|
| Example Repository For Finite State Verification Tools |
|
|
| Aubjex Static Analysis |
|
|
| Static Analysis of Upper and Lower Bounds on Dependences and Parallelism |
|
|
| Static Analysis And Software Assurance |
|
|
| Structural Static Analysis |
|
|
| Applications Of Static Analysis To Concurrency Control And Recovery In Objectbase Systems |
|
|
| Improving Java Programming language Code Using Static Analysis |
|
|
| Static Analysis Tables |
|
|
| Detection By Static Analysis |
|
|
| A Gentle Introduction To Static Analysis And Logic Programming |
|
|
| Applying Static Analysis Techniques For Inferring Termination Conditions Of Logic Programs |
|
|
| Type Inference And Static Analysis For Object-Oriented Software |
|
|
| A Toolkit For Static Analysis Constraint Logic Programs |
|
|
| Programme To "Nonlocal Automated Comparative Static Analysis" |
|
|
| Abstract Compilation: A New Implementation Paradigm For Static analysis |
|
|
| Static Analysis Applied To Java |
|
|
| An Efficient Static Analysis Algorithm To Detect Redundant Memory Operations |
|
|
| Static Analysis Of Object-Oriented Programs |
|
|
| Static Analysis For Guarded Code |
|
|
| Elimination Of Redundant Messages With A Two-Pass Static Analysis Algorithm |
|
|
| Static Analysis And Automatic Code Generation For Improved Fortran 90 and C++ Interoperability |
|
|
| Combining Static Analysis And Model Checking For Software Analysis |
|
|
| Applying Static Analysis To Large-Scale Industrial Programs |
|
|
| Static Analysis For Object-Oriented languages |
|
|
| Static Analysis For Program Generation Templates |
|
|
| Static Analysis Analysis Of Models, Data Flow Analyses, Finite State Verification |
|
|
| An Algebraic Approach To The Static Analysis Of Concurrent Software |
|
|
| Towards Software Testability Based On Static analysis |
|
|
| Applying Static Analysis To Software Architectures |
|
|
| Comparison Of Static Analysis Results Based On Different Models |
|
|
| An ASIS-Based Static Analysis Tool For High-Integrity Systems |
|
|
| A Static Analysis Method For A Classical Linear Logic Programming Language |
|
|
| Static Analysis Tools |
|
|
| Static Analysis And Validation Of Composite Behaviors In Composite Technology |
|
|
| Metrowerks Software Analysis Tools And Debug Probes |
|
|
| Code Coverage Analysis |
|
|
| Software Analysis And Formal Methods |
|
|
| A Survey Of Data-Flow Analysis Techniques |
|
|
| Data Flow Analysis For Reverse Engineering |
|
|
| Data Flow Analysis |
|
|
| Data Flow Analysis Frameworks Specification |
|
|
| Data Flow Analysis For Verifying Correctness Properties Of Concurrent Programs |
|
|
| The Combining DAG: A Technique For Parallel Data Flow Analysis |
|
|
| Implementation Techniques For Efficient Data-Flow Analysis Of Large Programs |
|
|
| Optimal Data Flow Analysis Via Observational Equivalence |
|
|
| Dynamic Data Flow Analysis |
|
|
| Data Flow Analysis Of Parallel Programs |
|
|
| DAFIA II - Further Development Data Flow Analysis For Integrated Assessments |
|
|
| An Incremental Flow- and Context-sensitive Pointer Aliasing Analysis |
|
|
| Hierarchical Data Flow Analysis for OO Programs |
|
|
| Data Flow Analysis For A Goto-Less Program |
|
|
| Error Detection By Data Flow Analysis Restricted To Executable Paths |
|
|
| Efficient Composite Data Flow Analysis Applied To Concurrent Programs |
|
|
| An Algorithm Of Programming Data Flow Analysis Based On Data Flow Expression |
|
|
| Data Flow Analysis & DFDs |
|
|
| Data-Flow Analysis for Constraint Logic-Based Languages |
|
|
| Logic Programming, Data-Flow Analysis and Equality Theories |
|
|
| Deferred Data Flow Analysis |
|
|
| Project: Data Flow Analysis Framework For Java: Summary |
|
|
| Data Flow Analysis Analyze Program To Find Out Facts |
|
|
| Data Flow Analysis Of Communicating Finite State Machines |
|
|
| Data-Flow Analysis Of Program Fragments |
|
|
| Eliminating Stale Data References Through Array Data Flow Analysis |
|
|
| Concurrent Data-Flow Analysis |
|
|
| Applicability of Algebraic Transductions to Data-Flow Analysis |
|
|
| On The Practical Static Checker Of Semantic Run-Time Errors |
|
|
| Data Flow Analysis Of Java Programs In The Presence Of Exceptions |
|
|
| Data Flow Analysis, Part I |
|
|
| Data Flow Analysis For Checking Properties Of Concurrent Java Programs |
|
|
| Data Flow Analysis Of Secure Information-Flow |
|
|
| Interprocedural Data Flow Analysis |
|
|
| Verification & Validation - Data-Flow Approaches |
|
|
| C Checker Reference Manual |
|
|
| Global Data Flow Analysis |
|
|
| Data Flow Analysis Of A Logic-Based Specification |
|
|
| Data Flow Analysis Of Program Nets |
|
|
| Data Flow Analysis (Course Slides) |
|
|
| DFA&OPT-METAFrame: A Tool Kit for Program Analysis and Optimization |
|
|
| DSA: Data Flow And SQL Analysis |
|
|
| Improving Data Flow Analysis With Path Profiles |
|
|
| A Generic Architecture For Data Flow Analysis To Support Reverse Engineering |
|
|
| Preliminary Analysis Of The Security Of Data Flow Code Transformations |
|
|
| Data Flow And Data Dependence Analysis |
|
|
| Incremental Data Flow Analysis |
|
|
| FLAVERS: A Finite State Verification Technique For Software Systems |
|
|
| Bandera - Java Model Checker |
|
|
| Software Model Construction For Finite-State Verification |
|
|
| Comparing Finite State Verification Techniques For Concurrent Software |
|
|
| Tool-Supported Program Abstraction For Finite-State Verification |
|
|
| Automatic Verification Methods For Finite-State Systems: International Workshop |
|
|
| Can Finite-State System Verification Methods Help Cryptographic Protocol Analysis ? |
|
|
| Toward Synergy Of Finite State Verification And Testing |
|
|
| Property Specification Patterns For Finite State Verification |
|
|
| Testing Finite-State Machines: State Identification And Verification |
|
|
| Patterns In Property Specifications For Finite-State Verification |
|
|
| Synthesis And Verification Of Finite-State Machines |
|
|
| Automatic Verification Of Finite-State Concurrent Systems |
|
|
| Finite State Machine Verification using Non-Ideal Multiple Processor Machines |
|
|
| Automatic Verification Methods For Finite State Systems |
|
|
| Finite-State Morphology and Formal Verification |
|
|
| Unbounded Verification Results by Finite-State Compositional Techniques |
|
|
| Example Repository Of Finite-State Verification Tools |
|
|
| Finite-State Machine Software, Products And Projects |
|
|
| Finite-State Analysis Of SSL 3.0 |
|
|
|
| |
Engineering
Software Process ...
Software Life Cycle
Light Weight ...
Agile Methods
