Merge pull request #1 from os-checker/update-commit-time-preview

[bot] Update last commit time in README.md

README.md

@@ -17,23 +17,23 @@
 
 | Name | Description | Working on | Bug types | Technology | Last Commit Time |
 | -----| ----------- | ---------- | ----------| -----------| ----------- |
-| [clippy](https://github.com/rust-lang/rust-clippy) | A bunch of lints to catch common mistakes and improve your Rust code. Paper: [ICSE-Companion'24](https://dl.acm.org/doi/abs/10.1145/3639478.3643096) | HIR | Versatile | Pattern matching | 2025-01-17 |
-| [dylint](https://github.com/trailofbits/dylint) | Run Rust lints from dynamic libraries | HIR | Versatile | Pattern matching | 2025-01-16 |
+| [clippy](https://github.com/rust-lang/rust-clippy) | A bunch of lints to catch common mistakes and improve your Rust code. Paper: [ICSE-Companion'24](https://dl.acm.org/doi/abs/10.1145/3639478.3643096) | HIR | Versatile | Pattern matching | 2025-01-23 |
+| [dylint](https://github.com/trailofbits/dylint) | Run Rust lints from dynamic libraries | HIR | Versatile | Pattern matching | 2025-01-21 |
 
 ## Static Checkers
 
 | Name | Description | Working on | Bug Types | Technology | Maintenance |
 | -----| ----------- | ---------- | ----------|-----------| ----------- |
 | [MIRAI](https://github.com/endorlabs/MIRAI) | Rust mid-level IR Abstract Interpreter | MIR | Panic, Security bugs, Correctness | Abstract Interpretation | 2025-01-11 |
 | [lockbud](https://github.com/BurtonQin/lockbud) | Statically detect common memory and concurrrency bugs in Rust. Paper: [Safety Issues in Rust, TSE'24](https://songlh.github.io/paper/rust-tse.pdf) | MIR | Double-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic Locations | Data-flow Analysis | 2025-01-13 |
-|[RAP (formerly SafeDrop)](https://github.com/Artisan-Lab/RAP) | Rust Analysis Platform. Paper: [SafeDrop, TOSEM'22](https://dl.acm.org/doi/10.1145/3542948) | MIR | Use-After-Free, Double-Free | Data-flow Analysis | 2025-01-17 |
+|[RAP (formerly SafeDrop)](https://github.com/Artisan-Lab/RAP) | Rust Analysis Platform. Paper: [SafeDrop, TOSEM'22](https://dl.acm.org/doi/10.1145/3542948) | MIR | Use-After-Free, Double-Free | Data-flow Analysis | 2025-01-18 |
 |[RCanary](https://github.com/Artisan-Lab/rCanary) | Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. [RCanary, TSE'24](https://arxiv.org/pdf/2308.04787) | HIR, MIR | Memory Leaks | Static Program Analysis, Model Checking | 2023-09-11 |
 |[Rudra](https://github.com/sslab-gatech/Rudra)| Rust Memory Safety & Undefined Behavior Detection. Paper: [Rudra, SOSP'21](https://dl.acm.org/doi/abs/10.1145/3477132.3483570) | HIR, MIR | Memory safety when panicked, Higher Order Invariant, Send Sync Variance | Data-flow Analysis | 2024-02-12 |
 |[Yuga](https://github.com/vnrst/Yuga) | Automatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: [Yuga, ICSE'24](https://arxiv.org/abs/2310.08507) | HIR, MIR |  Lifetime Annotation Bugs | Data-flow Analysis | 2024-04-01 |
 |[MirChecker](https://github.com/lizhuohua/rust-mir-checker)| A Simple Static Analysis Tool for Rust. Paper: [MirChecker, CCS'21](https://dl.acm.org/doi/10.1145/3460120.3484541) | MIR | Panic (including numerical), Lifetime Corruption (memory issues) | Abstract Interpretation | 2024-05-24 |
 |[FFIChecker](https://github.com/lizhuohua/rust-ffi-checker) | A Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: [FFIChecker, ESORICS'22](https://dl.acm.org/doi/10.1007/978-3-031-17143-7_33) | LLVM IR | Memory issues across the Rust/C FFI | Abstract Interpretation | 2022-05-31 |
 |[RUPTA](https://github.com/rustanlys/rupta) | Supports pointer/alias analysis for Rust, operating on Rust MIR. It currently offers callsite-based pointer analysis. Paper: [RUPTA, CC'24](https://dl.acm.org/doi/10.1145/3640537.3641574) | MIR | Not bugs, for callgraph construction| Callsite-based pointer analysis | 2024-12-02 |
-|[Charon](https://github.com/AeneasVerif/charon) | Interface with the rustc compiler for the purpose of program verification. Paper: [Charon](https://arxiv.org/abs/2410.18042) | MIR, LLBC | An Analysis Framework for Rust | Convert MIR to LLBC for analysis | 2025-01-17 |
+|[Charon](https://github.com/AeneasVerif/charon) | Interface with the rustc compiler for the purpose of program verification. Paper: [Charon](https://arxiv.org/abs/2410.18042) | MIR, LLBC | An Analysis Framework for Rust | Convert MIR to LLBC for analysis | 2025-01-23 |
 |[Cocoon](https://github.com/PLaSSticity/Cocoon-implementation) | Static Information Flow Control in Rust. Paper: [Cocoon, OOPSLA'24](https://dl.acm.org/doi/pdf/10.1145/3649817) | Rust Soure Code | Secrecy Leaks | Rust’s type system and procedural macros  | 2024-03-20 |
 |[rustsp_analyzer](https://github.com/Artisan-Lab/rustsp_analyzer) | Fearless Unsafe. A More User-friendly Document for Unsafe Rust Programming Base on Refined Safety Properties. Paper: [Fearless Unsafe](https://arxiv.org/pdf/2412.06251) | HIR | Safety Properties | Summarization | 2025-01-01 |
 |[AtomVChecker](https://github.com/AtomVChecker/rust-atomic-study/tree/main/section-5-detection/AtomVChecker) | Statically detect memory ordering misuses for Rust. Paper: [AtomVChecker, ISSRE'24](https://ieeexplore.ieee.org/document/10771495) | MIR | Atomic concurrency bugs and performance loss due to memory ordering misuse | Data-flow Analysis | 2024-09-12 |
@@ -56,11 +56,11 @@ Academic Papers (source code not found yet)
 
 | Name | Description | Working on | Bug Types | Technology | Last Commit Time |
 | -----| ----------- | ---------- | ----------| -----------| ----------- |
-| [miri](https://github.com/rust-lang/miri) | An interpreter for Rust's mid-level intermediate representation | MIR | Undefined Behavior | Abstract Interpretation | 2025-01-15 |
+| [miri](https://github.com/rust-lang/miri) | An interpreter for Rust's mid-level intermediate representation | MIR | Undefined Behavior | Abstract Interpretation | 2025-01-23 |
 | [cargo-careful](https://github.com/RalfJung/cargo-careful) | Execute Rust code carefully, with extra checking along the way | - | Undefined Behavior | Enable Debug Assertion in std | 2024-08-10 |
-| [cargo-fuzz](https://github.com/rust-fuzz/cargo-fuzz) | Command line helpers for fuzzing | - | - | Fuzzing | 2024-11-04 |
+| [cargo-fuzz](https://github.com/rust-fuzz/cargo-fuzz) | Command line helpers for fuzzing | - | - | Fuzzing | 2025-01-22 |
 | [Loom](https://github.com/tokio-rs/loom)| Concurrency permutation testing tool for Rust. | Source Code | Concurrency Bugs | Permutation testing | 2024-12-27 |
-| [Shuttle](https://github.com/awslabs/shuttle) | A library for testing concurrent Rust code. Paper [A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf) | Source Code | Concurrency Bugs | Randomized testing | 2024-12-06 |
+| [Shuttle](https://github.com/awslabs/shuttle) | A library for testing concurrent Rust code. Paper [A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf) | Source Code | Concurrency Bugs | Randomized testing | 2024-12-05 |
 | [ERASAN](https://github.com/S2-Lab/ERASan) | Efficient Rust Address Sanitizer. Paper: [IEEES&P'24](https://www.computer.org/csdl/proceedings-article/sp/2024/313000a239/1WPcYZde4BW) | - | Memory Access Bugs | Fuzzing | 2024-07-10 |
 | [Automated-Fuzzer](https://github.com/qarmin/Automated-Fuzzer) | Simple tool to create broken files and checking them with special apps | - | Panic | Fuzzing | 2025-01-13 |
 | [RULF](https://github.com/Artisan-Lab/RULF)| Fuzz Target Generator for Rust libraries. Paper: [RULF, ASE'21](https://dl.acm.org/doi/abs/10.1109/ASE51524.2021.9678813) | - | Out-of-bound, Panic (including arithmetic) | Fuzzing | 2023-11-09 |
@@ -93,18 +93,18 @@ Academic Papers (source code not found yet)
 
 | Name | Description | Working on | Bug Types | Technology | Last Commit Time |
 | -----| ----------- | ---------- | ----------| -----------| ----------- |
-| [kani](https://github.com/model-checking/kani/) | The Kani Rust Verifier is a bit-precise model checker for Rust. Paper: [kani, ICSE-SEIP'22](https://dl.acm.org/doi/abs/10.1145/3510457.3513031)| MIR | Memory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)  | Model Checking | 2025-01-17 |
+| [kani](https://github.com/model-checking/kani/) | The Kani Rust Verifier is a bit-precise model checker for Rust. Paper: [kani, ICSE-SEIP'22](https://dl.acm.org/doi/abs/10.1145/3510457.3513031)| MIR | Memory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)  | Model Checking | 2025-01-22 |
 | [prusti](https://github.com/viperproject/prusti-dev) | A static verifier for Rust, based on the Viper verification infrastructure. Paper: [prusti, NFM'22 ](https://link.springer.com/chapter/10.1007/978-3-031-06773-0_5) | Viper | Panic (inluding arithmetic), User-specified assertions | Symbolic Execution  | 2024-03-26 |
-| [crux-mir](https://github.com/GaloisInc/crucible/tree/master/crux-mir) | A static simulator for Rust programs. Paper: [crux](https://arxiv.org/abs/2410.18280) | - | - | Symbolic Testing | 2025-01-09 |
-| [verus](https://github.com/verus-lang/verus) | Verified Rust for low-level systems code. Paper: [verus, OOPSLA'23](https://dl.acm.org/doi/pdf/10.1145/3586037), [SOSP'24](https://www.microsoft.com/en-us/research/publication/verus-a-practical-foundation-for-systems-verification/) | - | - | SMT-based Verification<sup>5</sup> | 2025-01-17 |
+| [crux-mir](https://github.com/GaloisInc/crucible/tree/master/crux-mir) | A static simulator for Rust programs. Paper: [crux](https://arxiv.org/abs/2410.18280) | - | - | Symbolic Testing | 2025-01-23 |
+| [verus](https://github.com/verus-lang/verus) | Verified Rust for low-level systems code. Paper: [verus, OOPSLA'23](https://dl.acm.org/doi/pdf/10.1145/3586037), [SOSP'24](https://www.microsoft.com/en-us/research/publication/verus-a-practical-foundation-for-systems-verification/) | - | - | SMT-based Verification<sup>5</sup> | 2025-01-23 |
 | [flux](https://github.com/flux-rs/flux) | flux is a refinement type checker for Rust. Paper: [flux, PLDI'23](https://dl.acm.org/doi/10.1145/3591283)| - | - | - | 2025-01-14 |
-| [Aeneas](https://github.com/AeneasVerif/aeneas) | A verification toolchain for Rust programs. Paper: [Aeneas, ICFP'22](https://dl.acm.org/doi/abs/10.1145/3547647), [ICFP'24](https://dl.acm.org/doi/abs/10.1145/3674640) | LLBC (for safe Rust only) | - | - | 2025-01-17 |
+| [Aeneas](https://github.com/AeneasVerif/aeneas) | A verification toolchain for Rust programs. Paper: [Aeneas, ICFP'22](https://dl.acm.org/doi/abs/10.1145/3547647), [ICFP'24](https://dl.acm.org/doi/abs/10.1145/3674640) | LLBC (for safe Rust only) | - | - | 2025-01-21 |
 | [RustBelt](https://gitlab.mpi-sws.org/iris/lambda-rust/) | Formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: [RustBelt, POPL'18](https://dl.acm.org/doi/10.1145/3158154) | 𝜆Rust| - | - | 2024-12-13 |
 | [RustHorn](https://github.com/hopv/rust-horn) | A CHC-based automated verifier for Rust [RustHorn, TOPLAS'21](https://dl.acm.org/doi/full/10.1145/3462205) | MIR | - | - | 2024-08-27 |
-| [Creusot](https://github.com/creusot-rs/creusot) | A deductive verifier for Rust code. [Creusot, ICFEM'22](https://inria.hal.science/hal-03737878/file/main.pdf) | WhyML | Panics, overflows, Assertion failures | Deductive Verification | 2025-01-17 |
+| [Creusot](https://github.com/creusot-rs/creusot) | A deductive verifier for Rust code. [Creusot, ICFEM'22](https://inria.hal.science/hal-03737878/file/main.pdf) | WhyML | Panics, overflows, Assertion failures | Deductive Verification | 2025-01-23 |
 | [RustHornBelt](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/masters/rusthornbelt) | A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: [RustHornBelt, PLDI'22](https://dl.acm.org/doi/10.1145/3519939.3523704)| 𝜆Rust | - | - | 2023-02-14 |
 | [RefinedRust<sup>1</sup>](https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev) | A Type System for High-Assurance Verification of Rust Programs. Paper: [RefinedRust, PLDI'24](https://dl.acm.org/doi/10.1145/3656422)| Radium | - | - | 2025-01-03 |
-| [VeriFast<sup>2</sup>](https://github.com/verifast/verifast) | Research prototype tool for modular formal verification of C and Java programs. Paper: [VeriFast, NFM'11](https://doi.org/10.1007/978-3-642-20398-5_4)| - | - | Symbolic Execution | 2025-01-17 |
+| [VeriFast<sup>2</sup>](https://github.com/verifast/verifast) | Research prototype tool for modular formal verification of C and Java programs. Paper: [VeriFast, NFM'11](https://doi.org/10.1007/978-3-642-20398-5_4)| - | - | Symbolic Execution | 2025-01-22 |
 | [mendel-verifier](https://github.com/viperproject/mendel-verifier) | Capability-based verifier for safe Rust clients of interior mutability. Paper: [Poli](https://arxiv.org/abs/2405.08372), [Thesis](https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/703796/Poli2024.pdf?sequence=3&isAllowed=y)| Viper | Interior Mutability | Symbolic Execution | 2024-07-16 |
 | [silver-sif-extension](https://github.com/viperproject/silver-sif-extension) | Extension of the Viper language with modular product programs and information flow specifications. Paper: [Thesis](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Till_Arnold_MA_Report.pdf)| Viper | Differential Privacy | Symbolic Execution | 2023-08-21 |