Daniel Kröning, Corina S. Pasareanu
Proceedings of the 27th International Conference on Computer Aided Verification, Part I
CAV, 2015.
@proceedings{CAV-p1-2015, address = "San Francisco, California, USA", doi = "10.1007/978-3-319-21690-4", editor = "Daniel Kröning and Corina S. Pasareanu", isbn = "978-3-319-21689-8", publisher = "{Springer International Publishing}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the 27th International Conference on Computer Aided Verification, Part I}", volume = 9206, year = 2015, }
Event page: http://i-cav.org/2015/
Contents (44 items)
- CAV-2015-GardnerSWW #javascript #specification
- A Trusted Mechanised Specification of JavaScript: One Year On (PG, GS, CW, TW), pp. 3–10.
- CAV-2015-CookKP #automation #infinity #on the #verification
- On Automation of CTL* Verification for Infinite-State Systems (BC, HK, NP), pp. 13–29.
- CAV-2015-FinkbeinerRS #algorithm #model checking
- Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.
- CAV-2015-DietschHLP #approach #ltl #model checking #modulo theories
- Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
- CAV-2015-Durand-Gasselin #model checking
- Model Checking Parameterized Asynchronous Shared-Memory Systems (ADG, JE, PG, RM), pp. 67–84.
- CAV-2015-KonnovVW #abstraction #algorithm #distributed #model checking #smt
- SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms (IK, HV, JW), pp. 85–102.
- CAV-2015-JainM #refinement
- Skipping Refinement (MJ, PM), pp. 103–119.
- CAV-2015-RandourRS #markov #multi #process #query
- Percentile Queries in Multi-dimensional Markov Decision Processes (MR, JFR, OS), pp. 123–139.
- CAV-2015-ChatterjeeIP #algorithm #constant #graph #performance #verification
- Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs (KC, RIJ, AP), pp. 140–157.
- CAV-2015-BrazdilCCFK #learning #markov #process
- Counterexample Explanation by Learning Small Strategies in Markov Decision Processes (TB, KC, MC, AF, JK), pp. 158–177.
- CAV-2015-GleissenthallKR #verification
- Symbolic Polytopes for Quantitative Interpolation and Verification (KvG, BK, AR), pp. 178–194.
- CAV-2015-AbateBCK #adaptation #analysis #markov #network
- Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks (AA, LB, MC, MZK), pp. 195–213.
- CAV-2015-DehnertJJCVBKA #named #parametricity #probability #synthesis
- PROPhESY: A PRObabilistic ParamEter SYnthesis Tool (CD, SJ, NJ, FC, MV, HB, JPK, EÁ), pp. 214–231.
- CAV-2015-ZhengGSTDZ #constraints #effectiveness #equation #regular expression #string
- Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints (YZ, VG, SS, OT, JD, XZ), pp. 235–254.
- CAV-2015-AydinBB #constraints #string
- Automata-Based Model Counting for String Constraints (AA, LB, TB), pp. 255–272.
- CAV-2015-GouwRBBH #java
- OpenJDK’s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case (SdG, JR, FSdB, RB, RH), pp. 273–289.
- CAV-2015-GrigoreK
- Tree Buffers (RG, SK), pp. 290–306.
- CAV-2015-GehrDV #commutative #learning #specification
- Learning Commutativity Specifications (TG, DD, MTV), pp. 307–323.
- CAV-2015-DasLLL #precise #verification
- Angelic Verification: Precise Verification Modulo Unknowns (AD, SKL, AL, YL), pp. 324–342.
- CAV-2015-GurfinkelKKN #framework #verification
- The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.
- CAV-2015-LahiriSH #automation #equivalence
- Automatic Rootcausing for Program Equivalence Failures in Binaries (SKL, RS, CH), pp. 362–379.
- CAV-2015-LeinoW #fine-grained #verification
- Fine-Grained Caching of Verification Results (KRML, VW), pp. 380–397.
- CAV-2015-SinghG #predict #programming
- Predicting a Correct Program in Programming by Example (RS, SG), pp. 398–414.
- CAV-2015-OulamaraV #abstract interpretation
- Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation (MO, AJV), pp. 415–430.
- CAV-2015-FinkbeinerGO #distributed #named #synthesis
- Adam: Causality-Based Synthesis of Distributed Systems (BF, MG, ERO), pp. 433–439.
- CAV-2015-Saha0M #learning #named
- Alchemist: Learning Guarded Affine Functions (SS, PG, PM), pp. 440–446.
- CAV-2015-SebastianiT #modulo theories #named #optimisation
- OptiMathSAT: A Tool for Optimization Modulo Theories (RS, PT), pp. 447–454.
- CAV-2015-OzkanET #android #debugging
- Systematic Asynchrony Bug Exploration for Android Apps (BKO, ME, ST), pp. 455–461.
- CAV-2015-AbdullaACHRRS #constraints #named #smt #string
- Norn: An SMT Solver for String Constraints (PAA, MFA, YFC, LH, AR, PR, JS), pp. 462–469.
- CAV-2015-MasciOZJCT #human-computer
- PVSio-web 2.0: Joining PVS to HCI (PM, PO, YZ, PLJ, PC, HWT), pp. 470–478.
- CAV-2015-BabiakBDKKM0S
- The Hanoi Omega-Automata Format (TB, FB, ADL, JK, JK, DM, DP, JS), pp. 479–486.
- CAV-2015-IsbernerHS #automaton #framework #learning #open source
- The Open-Source LearnLib — A Framework for Active Automata Learning (MI, FH, BS), pp. 487–495.
- CAV-2015-MajumdarW #bound #model checking #named #source code
- Bbs: A Phase-Bounded Model Checker for Asynchronous Programs (RM, ZW), pp. 496–503.
- CAV-2015-Tiwari #abstraction
- Time-Aware Abstractions in HybridSal (AT), pp. 504–510.
- CAV-2015-ReinkingP #approach #program repair
- A Type-Directed Approach to Program Repair (AR, RP), pp. 511–517.
- CAV-2015-BozzanoCPJKPRT #analysis #design #safety
- Formal Design and Safety Analysis of AIR6110 Wheel Brake System (MB, AC, AFP, DJ, GK, TP, RR, ST), pp. 518–535.
- CAV-2015-DuggiralaFM0 #challenge #verification
- Meeting a Powertrain Verification Challenge (PSD, CF, SM, MV), pp. 536–543.
- CAV-2015-FisherKPW #execution #network
- Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data (JF, ASK, NP, SW), pp. 544–560.
- CAV-2015-DemyanovaPVZ #benchmark #empirical #metric #tool support #verification
- Empirical Software Metrics for Benchmarking of Verification Tools (YD, TP, HV, FZ), pp. 561–579.
- CAV-2015-KarbyshevBIRS #invariant #proving
- Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.
- CAV-2015-BozzanoCGM #analysis #modelling #performance #safety
- Efficient Anytime Techniques for Model-Based Safety Analysis (MB, AC, AG, CM), pp. 603–621.
- CAV-2015-BeyerW #invariant
- Boosting k-Induction with Continuously-Refined Invariants (DB, MD, PW), pp. 622–640.
- CAV-2015-VizelGM #performance
- Fast Interpolating BMC (YV, AG, SM), pp. 641–657.
- CAV-2015-ChenHWZ #generative #invariant #polynomial
- Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation (YFC, CDH, BYW, LZ), pp. 658–674.
8 ×#verification
6 ×#named
5 ×#model checking
4 ×#learning
3 ×#algorithm
3 ×#analysis
3 ×#constraints
3 ×#invariant
3 ×#markov
3 ×#performance
6 ×#named
5 ×#model checking
4 ×#learning
3 ×#algorithm
3 ×#analysis
3 ×#constraints
3 ×#invariant
3 ×#markov
3 ×#performance