Notes
- Abstract interpretation
- ACL2 theorem prover
- Activation function
- AFL fuzzer
- Alias analysis
- Alloy verifier
- angr verifier
- Annotation burden
- Absence of RunTime Errors (AoRTE)
- Arm architecture
- Arm Architecture Specification Language (ASL)
- Aspect oriented programming
- Attention function
- Auto active verification
- Auto-encoder model
- Automatic exploit generation
- Binary Analysis Platform (BAP)
- Binary Decision Diagrams (BDD)
- Beneš network
- Bi-abduction
- Binary analysis
- Binary instrumentation
- Binary lifter
- BinRec binary lifter
- BLAST verifier
- Bilingual evaluation understudy (BLEU)
- BlueSpec SystemVerilog
- Boogie verifier
- Bounded model-checking
- Bounded verification
- Büchi automaton
- Bug localization
- Cactus plot / Survival plot
- CakeML compiler
- Capabilities
- Capstone disassembler
- Case splitting
- CBMC verifier
- CEGAR (Counter-Example Guided Abstraction Refinement)
- Chalice verifier
- CHERI architecture
- CHERI-Flute
- CIL tool
- CIVL verifier
- Convolutional neural network (CNN)
- CompCert compiler
- Compiler verification
- Compiler
- Concolic execution
- Concurrent separation logic
- Continuations
- Contract driven development
- Coq theorem prover
- Corral verifier
- CPAchecker verifier
- CPU verification
- Cray architecture
- CREST verifier
- Cryptography
- CUTE verifier
- CVC4 solver
- Cyclone language
- Dafny verifier
- Dagger binary lifter
- DARPA Cyber Grand Challenge (CGC)
- DART verifier
- Data parallelism
- Decidability ceiling
- Decoupled Access Execute
- Decoupling
- Deep neural networks
- Defunctionalization
- Dependency injection
- Dependent type
- Differential Power Analysis
- Differential testing
- DigFuzz fuzzer
- Distributed Shared Memory
- Domain Specific Language (DSL)
- Driller verifier
- Dynamic binary translation (DBT)
- DynamoRIO binary instrumentation tool
- Effects
- Equality graphs (egraphs)
- Embedding
- Entropy
- Equality saturation
- Events
- EXE symbolic executor
- Extended static checking (ESC)
- Foreign function interface
- Formal specification
- FShell Query Language (FQL)
- Fractional permissions
- Frama-C verifier
- Frame rule
- Friction diagram
- Functional Reactive Programming (FRP)
- Fuzz testing
- Generative adversarial neural network (GAN)
- Garbage collection
- Gating network
- Genetic algorithm
- Ghost code
- Google papers and infrastructure
- Hardware Faults
- Hardware trojan
- Hardware
- Haskell language
- HOL theorem prover
- Horizontal side channel analysis
- Horn clauses
- Human factors
- Hybrid testing
- Hyperproperty
- Hypervisor
- Implicit dynamic frames
- Incorrectness logic
- Information flow
- Instruction set architecture
- Intel
- Interactive theorem prover
- Intermediate verification language
- Interpolation
- Interposition
- Invariants
- ISA specification
- Isabelle theorem prover
- Instruction Set Processor (ISP)
- Itanium architecture
- Ivy verifier
- JasperGold bounded model checker
- Java PathFinder
- JavaScript programming language
- KLEE verifier
- Kripke structure
- L3 specification language
- Language based security
- Lazy initialization of symbolic values
- Leakage contracts
- Lean theorem prover
- Linear logic
- Liquid type
- LISA
- LLBMC verifier
- LLVM compiler
- LLVM-MCtoLL binary lifter
- Loop fusion
- Loop invariant
- Long short-term memory (LSTM)
- Machine learning
- Magic wand
- Malware analysis
- Mayhem
- McSema binary lifter
- Memory coherence
- Memory management
- Memory safety
- Microarchitecture
- MILP solver
- Multiple Instruction Multiple Data (MIMD)
- MIPS architecture
- MIR interpreter (miri)
- MIR
- Mixture of experts
- Multi-layer perceptrons (MLP)
- Model based testing
- Model checking
- Model counting
- Modular verification
- Module system
- Mutation testing
- Natural language
- Networks
- Neural network
- Natural language processing (NLP)
- Non-interference
- Non leakage
- NOVA hypervisor
- Omega library
- Operating systems
- Over-approximation
- Ownership types
- Parallelism
- Partial Order Reduction
- Paxos distributed consensus algorithm
- PDP11 architecture
- Permission accounting
- Permission logic
- Phantom types
- PIN binary instrumentation tool
- Pipeline parallelism
- Power Virus
- Power-PC architecture
- Proof carrying code
- Property-based testing
- Prusti verifier
- PVS theorem prover
- PyTorch
- QEMU
- QSYM verifier
- Quantum computing
- QUIC protocol
- Reachability
- Reference counting
- Refinement types
- Regions
- Rectified linear unit (RELU)
- Remill binary lifting library
- Remote procedure call (RPC)
- reopt binary lifter
- Requirements specification
- Resonant frequency
- RetDec decompiler
- Reverse engineering
- rev.ng reverse engineering tool
- Rewrite rules
- RISC architecture
- RISC-V architecture
- Recurrent neural network (RNN)
- Roofline performance model
- Rosette solver
- RowHammer
- RTL
- Rust language
- Rust unsafe code
- RustBelt verifier
- S2E verifier
- SAGE verifier
- Sail ISA specification language
- Sanitizer
- SAT solver
- Saturn verifier
- Savior hybrid testing tool
- Software Defined Radio (SDR)
- SeaHorn verifier
- Search based test generation
- SecondWrite binary lifter
- Security
- Self composition
- Separation logic
- Serval solver-based verifier
- Shape analysis
- Side Channel
- Single Instruction Multiple Data (SIMD)
- Specification language for encoding and decoding (SLED)
- SMACK verifier
- Smallfoot verifier
- SMT-LIB format
- SMT solver
- Soft max
- Sparc architecture
- Sparse model
- Spec# project
- Speculative execution
- State merging
- Stochastic gradient descent (SGD)
- Stream Processing
- Superoptimizer
- Survey
- Software Verification Competition (SV-COMP)
- Swarm verification
- Symbolic evaluation
- Symbolic execution
- Symbolic memory
- Symbolic model checking
- Symbolic Quick Error Detection (Symbolic QED)
- Symbolic trajectory evaluation
- SymCC
- Synthesis
- Systematization of Knowledge (SoK)
- SystemVerilog Assertions (SVA)
- SystemVerilog
- TCG (Tiny Code Generator) intermediate representation
- Temporal logic
- Tensor
- TensorFlow
- Test-case reduction
- Software Testing Competition (Test-Comp)
- Test doubles (fakes, mocks and stubs)
- Test driven development
- Test generation
- Testability
- Threads
- Tensor Processing Unit (TPU)
- Transformer machine learning model
- Translation validation
- Total store order (TSO)
- Turing Award
- Type Inference
- Typed assembly language
- UCLID5 tool
- Undefined behaviour
- Under-approximation
- Unit tests
- Usability research
- uSpec
- Valgrind binary instrumentation tool
- Valgrind
- VCC verifier
- Vector architecture
- VeriFast verifier
- Verification tool competition
- Verification condition generator
- Verification performance of code
- Verification profiling of code
- Verification
- Verified compilers
- Verifier performance
- Vertical side channel analysis
- Viper verifier
- Very Long Instruction Word (VLIW)
- Weak memory
- Weakest precondition
- Weird machines
- Why3 verifier
- x86 architecture
- XED x86 encoding/decoding library
- XNNPACK
- Z3 theorem prover
- zydis x86 decoder/disassembler library