Tag #correctness
273 papers:
- ICPC-2019-PetersonLD #named #specification
- CCSpec: a correctness condition specification tool (CLP, PL, DD), pp. 220–230.
- FM-2019-DerrickDDSW #concurrent #data type #persistent #verification
- Verifying Correctness of Persistent Concurrent Data Structures (JD, SD, BD, GS, HW), pp. 179–195.
- ICFP-2019-0001A #compilation #functional #theorem
- The next 700 compiler correctness theorems (functional pearl) (DP0, AA), p. 29.
- POPL-2019-RaadDRLV #concurrent #consistency #declarative #library #memory management #modelling #on the #specification #verification
- On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models (AR, MD, LR, OL, VV), p. 31.
- ICSE-2019-LeB00LP #assessment #on the #reliability
- On reliability of patch correctness assessment (XBDL, LB, DL0, XX0, SL, CSP), pp. 524–535.
- SANER-2018-KuleszK0 #approach #evolution #semantics #spreadsheet
- Spreadsheet guardian: An approach to protecting semantic correctness throughout the evolution of spreadsheets (journal-first abstract) (DK, VK, SW0), p. 476.
- POPL-2018-FluckigerSYGAV #optimisation
- Correctness of speculative optimizations with dynamic deoptimization (OF, GS, MHY, AG, AA, JV), p. 28.
- POPL-2018-Lee0A #automation #implementation #on the #proving
- On automatically proving the correctness of math.h implementations (WL0, RS0, AA), p. 32.
- ICSE-2018-DanglotPBM #behaviour #case study #runtime
- Correctness attraction: a study of stability of software behavior under runtime perturbation (BD, PP, BB, MM), p. 481.
- ICSE-2018-XiongLZ00 #identification #program repair
- Identifying patch correctness in test-based program repair (YX, XL, MZ, LZ0, GH0), pp. 789–799.
- SLE-2018-Rinard #approach #reliability
- A new approach for software correctness and reliability (MCR), pp. 1–2.
- CASE-2018-ThonnessenRRSK #algorithm #multi #specification
- Correctness Properties and Exemplified Applicability of a Signal Matching Algorithm with Multidimensional Tolerance Specifications (DT, NR, SR, AS, SK), pp. 1197–1202.
- ESOP-2018-FrancoCDVW #concurrent
- Correctness of a Concurrent Object Collector for Actor Languages (JF, SC, SD, JV, TW), pp. 885–911.
- AdaEurope-2017-RoyuelaMQP #ada #safety
- OpenMP Tasking Model for Ada: Safety and Correctness (SR, XM, EQ, LMP), pp. 184–200.
- FM-2016-GomesS #algebra
- Modal Kleene Algebra Applied to Program Correctness (VBFG, GS), pp. 310–325.
- FSCD-2016-BrenasES #graph grammar #proving #term rewriting
- Proving Correctness of Logically Decorated Graph Rewriting Systems (JHB, RE, MS), p. 15.
- OOPSLA-2016-SergeyNBD #concurrent #hoare #specification
- Hoare-style specifications as correctness conditions for non-linearizable concurrent objects (IS, AN, AB0, GAD), pp. 92–110.
- SAS-2016-JournaultM #abstract interpretation #functional #matrix #source code #static analysis
- Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs (MJ, AM), pp. 257–277.
- FSE-2016-BeyerDDH #verification
- Correctness witnesses: exchanging verification results between verifiers (DB, MD, DD, MH), pp. 326–337.
- FASE-2016-PutterW #automaton #lts #verification
- Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique (SdP, AW), pp. 383–400.
- ICTSS-2016-PatelH #nondeterminism #problem
- Resolving the Equivalent Mutant Problem in the Presence of Non-determinism and Coincidental Correctness (KP, RMH), pp. 123–138.
- VLDB-2015-AkidauBCCFLMMPS #approach #bound #data flow #latency
- The Dataflow Model: A Practical Approach to Balancing Correctness, Latency, and Cost in Massive-Scale, Unbounded, Out-of-Order Data Processing (TA, RB, CC, SC, RFM, RL, SM, DM, FP, ES, SW), pp. 1792–1803.
- FM-2015-DerrickS #framework #memory management #modelling
- A Framework for Correctness Criteria on Weak Memory Models (JD, GS), pp. 178–194.
- CIG-2015-ChangHH #algorithm #analysis #case study #convergence #monte carlo
- Convergence and correctness analysis of Monte-Carlo tree search algorithms: A case study of 2 by 4 Chinese dark chess (HJC, CWH, TsH), pp. 260–266.
- GCM-2015-Flick #graph #on the #recursion #source code
- On Correctness of Graph Programs Relative to Recursively Nested Conditions (NEF), pp. 97–112.
- MoDELS-J-2011-HermannEOCDXGE15 #graph grammar
- Model synchronization based on triple graph grammars: correctness, completeness and invertibility (FH, HE, FO, KC, ZD, YX, SG, TE), pp. 241–269.
- ECOOP-2015-DongolDGS #architecture #concurrent #manycore
- Defining Correctness Conditions for Concurrent Objects in Multicore Architectures (BD, JD, LG, GS), pp. 470–494.
- LOPSTR-2015-SatoK0T #term rewriting
- Correctness of Context-Moving Transformations for Term Rewriting Systems (KS, KK, TA0, YT), pp. 331–345.
- ICSE-v2-2015-DialloGM
- Correctness and Relative Correctness (ND, WG, AM), pp. 591–594.
- SAC-2015-TakanoI #functional #lazy evaluation #semantics
- Thunk recycling for lazy functional languages: operational semantics and correctness (YT, HI), pp. 2079–2086.
- CGO-2015-HasabnisQS #architecture #code generation #specification
- Checking correctness of code generator architecture specifications (NH, RQ, RS), pp. 167–178.
- DAC-2015-RayYBB #design #security #validation
- Correctness and security at odds: post-silicon validation of modern SoC designs (SR, JY, AB, SB), p. 6.
- SOSP-2015-MinKLSK #debugging #file system #semantics
- Cross-checking semantic correctness: the case of finding file system bugs (CM, SK, BL, CS, TK), pp. 361–377.
- CADE-2015-MaricJM #higher-order #proving #using
- Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
- ICLP-J-2015-AngelisFPP #horn clause #imperative #proving #source code
- Proving correctness of imperative programs by linearizing constrained Horn clauses (EDA, FF, AP, MP), pp. 635–650.
- ISSTA-2015-QiLAR #analysis #generative
- An analysis of patch plausibility and correctness for generate-and-validate patch generation systems (ZQ, FL, SA, MCR), pp. 24–36.
- FLOPS-2014-Bahr #compilation #graph #proving #using
- Proving Correctness of Compilers Using Structured Graphs (PB), pp. 221–237.
- SEKE-2014-ZhouWLZ #empirical #probability #test coverage #testing
- An Empirical Study on the Test Adequacy Criterion Based on Coincidental Correctness Probability (XZ, LW, XL, JZ), pp. 632–635.
- ICMT-2014-OrejasP #graph grammar #incremental
- Correctness of Incremental Model Synchronization with Triple Graph Grammars (FO, EP), pp. 74–90.
- OOPSLA-2014-FeldthausM #interface #javascript #library #typescript
- Checking correctness of TypeScript interfaces for JavaScript libraries (AF, AM), pp. 1–16.
- HILT-2014-Ball #compilation #logic #research #verification
- Correctness via compilation to logic: a decade of verification at microsoft research (TB), pp. 69–70.
- PADL-2014-AreiasR #logic programming #on the #performance #source code
- On the Correctness and Efficiency of Lock-Free Expandable Tries for Tabled Logic Programs (MA, RR), pp. 168–183.
- DATE-2014-AltmeyerD #analysis #on the #precise #probability
- On the correctness, optimality and precision of Static Probabilistic Timing Analysis (SA, RID), pp. 1–6.
- TACAS-2014-BoenderC #algorithm #branch #on the
- On the Correctness of a Branch Displacement Algorithm (JB, CSC), pp. 605–619.
- LICS-CSL-2014-Ehrhard #proving
- A new correctness criterion for MLL proof nets (TE), p. 10.
- CBSE-2013-BurtonS #data type #mixin #using
- Correctness of intrusive data structures using mixins (EB, ES), pp. 53–58.
- WCRE-2013-SmithsonEAKB #trade-off
- Static binary rewriting without supplemental information: Overcoming the tradeoff between coverage and correctness (MS, KE, KA, AK, RB), pp. 52–61.
- ICFP-2013-Schmidt-SchaussS #haskell #implementation
- Correctness of an STM Haskell implementation (MSS, DS), pp. 161–172.
- GCM-J-2012-PoskittP #graph #source code #verification
- Verifying Total Correctness of Graph Programs (CMP, DP).
- AMT-2013-Gottmann0NBEEE #concurrent #graph grammar
- Correctness and Completeness of Generalised Concurrent Model Synchronisation Based on Triple Graph Grammars (SG, FH, NN, BB, CE, HE, TE), pp. 62–71.
- MoDELS-2013-BalabanM #composition #constraints #diagrams #multi #uml
- Simplification and Correctness of UML Class Diagrams — Focusing on Multiplicity and Aggregation/Composition Constraints (MB, AM), pp. 454–470.
- PEPM-2013-SulzmannNZ #abstraction #traceability
- Traceability and evidence of correctness of EDSL abstractions (MS, JNF, AZ), pp. 71–74.
- SAS-2013-FouilheMP #abstract domain #generative #performance
- Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra (AF, DM, MP), pp. 345–365.
- FM-2012-GiorginoS #algorithm #pointer
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction (MG, MS), pp. 202–216.
- ICEIS-v2-2012-CapelM #approach #automation #composition #model checking #safety #verification
- A Formal Compositional Verification Approach for Safety-Critical Systems Correctness — Model-Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software (MIC, LEMM), pp. 105–112.
- SEKE-2012-MiaoCLZZ #clustering #fault #identification #locality #testing
- Identifying Coincidental Correctness for Fault Localization by Clustering Test Cases (YM, ZC, SL, ZZ, YZ), pp. 267–272.
- ICSE-2012-EsteveKNPY #analysis #dependence #performance #safety
- Formal correctness, safety, dependability, and performance analysis of a satellite (MAE, JPK, VYN, BP, YY), pp. 1022–1031.
- DAC-2012-PurandareAH #proving #regular expression
- Proving correctness of regular expression accelerators (MP, KA, CH), pp. 350–355.
- PPoPP-2012-BurnimENS #named #nondeterminism #parallel #specification
- NDetermin: inferring nondeterministic sequential specifications for parallelism correctness (JB, TE, GCN, KS), pp. 329–330.
- ESOP-2012-BurckhardtGMY #concurrent #library #memory management
- Concurrent Library Correctness on the TSO Memory Model (SB, AG, MM, HY), pp. 87–107.
- ESOP-2012-HabermaierK #execution #on the
- On the Correctness of the SIMT Execution Model of GPUs (AH, AK), pp. 316–335.
- ICLP-J-2012-BaralDGG #algorithm #programming #set #λ-calculus
- Typed answer set programming λ calculus theories and correctness of inverse λ algorithms with respect to them (CB, JD, MAG, AG), pp. 775–791.
- ICST-2012-Bandyopadhyay #fault #locality
- Mitigating the Effect of Coincidental Correctness in Spectrum Based Fault Localization (AB), pp. 479–482.
- IJCAR-2012-RauSS #problem #program transformation #termination
- Correctness of Program Transformations as a Termination Problem (CR, DS, MSS), pp. 462–476.
- ISSTA-2012-StaatsHKR #comprehension #invariant
- Understanding user understanding: determining correctness of generated program invariants (MS, SH, MK, GR), pp. 188–198.
- KMIS-2011-AndreasikCU #health #semantics #web
- A Semantic Web Technologies-based System for Controlling the Correctness of Medical Procedures in Polish National Health Fund (JA, AC, SU), pp. 331–336.
- MoDELS-2011-HermannEOCDX #graph grammar
- Correctness of Model Synchronization Based on Triple Graph Grammars (FH, HE, FO, KC, ZD, YX), pp. 668–682.
- PLDI-2011-BurnimENS #named #nondeterminism #parallel #runtime #specification
- NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness (JB, TE, GCN, KS), pp. 401–414.
- ASE-2011-MacleanIG #animation #functional #pointer #source code
- The CORE system: Animation and functional correctness of pointer programs (EM, AI, GG), pp. 588–591.
- DATE-2011-NarayananZT #pattern matching #process #using
- Ensuring correctness of analog circuits in presence of noise and process variations using pattern matching (RN, MHZ, ST), pp. 1188–1191.
- ICLP-J-2011-Antoy #on the
- On the correctness of pull-tabbing (SA), pp. 713–730.
- ICSM-2010-Haller #implementation #information management #on the
- On the implementation and correctness of information system upgrades (KH), pp. 1–5.
- IFM-2010-DaumSS
- From Operating-System Correctness to Pervasively Verified Applications (MD, NS, MS), pp. 105–120.
- ICGT-2010-Radke #graph #source code
- Correctness of Graph Programs Relative to HR + Conditions (HR), pp. 410–412.
- CAiSE-2010-SidorovaST #concept #workflow
- Workflow Soundness Revisited: Checking Correctness in the Presence of Data While Staying Conceptual (NS, CS, NT), pp. 530–544.
- ECIR-2010-CoxZFH #approximate #query #using
- Improving Query Correctness Using Centralized Probably Approximately Correct (PAC) Search (IJC, JZ, RF, LKH), pp. 265–280.
- KR-2010-HuL #problem #reasoning
- A Correctness Result for Reasoning about One-Dimensional Planning Problems (YH, HJL).
- LOPSTR-2010-HerasPR #proving #set
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.
- PLDI-2010-RuwaseCGM #optimisation #tool support
- Decoupled lifeguards: enabling path optimizations for dynamic correctness checking tools (OR, SC, PBG, TCM), pp. 25–35.
- POPL-2010-Henzinger
- From Boolean to quantitative notions of correctness (TAH), pp. 157–158.
- SLE-2010-ErdwegO #parsing #tex
- Featherweight TeX and Parser Correctness (STE, KO), pp. 397–416.
- ICST-2010-MasriA #testing
- Cleansing Test Suites from Coincidental Correctness to Enhance Fault-Localization (WM, RAA), pp. 165–174.
- EDM-2009-CetintasSXH #low level #predict #problem
- Predicting Correctness of Problem Solving from Low-level Log Data in Intelligent Tutoring Systems (SC, LS, YPX, CH), pp. 230–239.
- LATA-2009-PardubskaPO #automaton #communication #on the #parallel
- On Parallel Communicating Grammar Systems and Correctness Preserving Restarting Automata (DP, MP, FO), pp. 660–671.
- SEFM-2009-DaumSS #implementation #operating system #realtime
- Implementation Correctness of a Real-Time Operating System (MD, NS, MS), pp. 23–32.
- ICFP-2009-BentonH #compilation
- Biorthogonality, step-indexing and compiler correctness (NB, CKH), pp. 97–108.
- GT-VMT-2009-EhrigHS #graph grammar #model transformation
- Completeness and Correctness of Model Transformations based on Triple Graph Grammars with Negative Application Conditions (HE, FH, CS), pp. 67–84.
- MoDELS-2009-EhrigEHP #graph grammar #model transformation #on the fly
- On-the-Fly Construction, Correctness and Completeness of Model Transformations Based on Triple Graph Grammars (HE, CE, FH, UP), pp. 241–255.
- MoDELS-2009-EhrigEHP #graph grammar #model transformation #on the fly
- On-the-Fly Construction, Correctness and Completeness of Model Transformations Based on Triple Graph Grammars (HE, CE, FH, UP), pp. 241–255.
- TOOLS-EUROPE-2009-KastnerATKB #approach #independence #product line
- Guaranteeing Syntactic Correctness for All Product Line Variants: A Language-Independent Approach (CK, SA, ST, MK, DSB), pp. 175–194.
- SAS-2009-Bouissou #algorithm #implementation #proving
- Proving the Correctness of the Implementation of a Control-Command Algorithm (OB), pp. 102–119.
- ICSE-2009-WangCCZ #fault #locality #refinement
- Taming coincidental correctness: Coverage refinement with context patterns to improve fault localization (XW, SCC, WKC, ZZ), pp. 45–55.
- CGO-2009-BoissinotDRDG #performance #quality
- Revisiting Out-of-SSA Translation for Correctness, Code Quality and Efficiency (BB, AD, FR, BDdD, CG), pp. 114–125.
- MSR-2008-ThomsonH #cvs
- Correctness of data mined from CVS (CT, MH), pp. 117–120.
- ICGT-2008-EhrigE #graph #model transformation #semantics #using
- Semantical Correctness and Completeness of Model Transformations Using Graph and Rule Transformation (HE, CE), pp. 194–210.
- SEKE-2008-PengDZ #behaviour #design pattern #implementation #verification
- Verifying Behavioral Correctness of Design Pattern Implementation (TP, JD, YZ), pp. 454–459.
- PEPM-2008-Voigtlander #proving #theorem
- Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.
- PPDP-2008-MontenegroPS #memory management #proving #type system
- A type system for safe memory management and its proof of correctness (MM, RP, CS), pp. 152–162.
- PPoPP-2008-GuerraouiK #memory management #on the #transaction
- On the correctness of transactional memory (RG, MK), pp. 175–184.
- CAV-2008-WienandWSKG #algebra #approach #proving
- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths (OW, MW, DS, WK, GMG), pp. 473–486.
- CSL-2008-Tranquilli #linear #logic #multi #semantics
- A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic (PT), pp. 246–261.
- LICS-2008-NauroisM #multi #proving
- Correctness of Multiplicative Additive Proof Structures is NL-Complete (PJdN, VM), pp. 476–485.
- VLDB-2007-SionBCK #named
- NS2: Networked Searchable Store with Correctness (RS, SB, BC, SK), pp. 1342–1345.
- VLDB-2007-WangYLLBIB #data access #database #fine-grained #on the #relational
- On the Correctness Criteria of Fine-Grained Access Control in Relational Databases (QW, TY, NL, JL, EB, KI, JWB), pp. 555–566.
- ITiCSE-2007-StallmannBRBGH #automaton #named #proving
- ProofChecker: an accessible environment for automata theory correctness proofs (MFS, SB, RDR, SB, MCG, SDH), pp. 48–52.
- ICALP-2007-ChuKM
- Checking and Spot-Checking the Correctness of Priority Queues (MC, SK, AM), pp. 728–739.
- IFM-2007-DunneG
- Lifting General Correctness into Partial Correctness is ok (SD, AG), pp. 215–232.
- RTA-2007-Schmidt-Schauss #calculus
- Correctness of Copy in Calculi with Letrec (MSS), pp. 329–343.
- ICEIS-DISI-2007-CarterO #on the #workflow
- On correctness criteria for workflow (BMC, MEO), pp. 315–322.
- SEKE-2007-FuDASH #approach #java #validation
- An Approach to Validating Translation Correctness From SAM to Java (YF, ZD, GAG, LS, XH), p. 45–?.
- SIGIR-2007-NtoulasC #policy
- Pruning policies for two-tiered inverted index with correctness guarantee (AN, JC), pp. 191–198.
- AdaEurope-2007-BordinV #approach #metamodelling #realtime
- Correctness by Construction for High-Integrity Real-Time Systems: A Metamodel-Driven Approach (MB, TV), pp. 114–127.
- SIGAda-2007-Chapman07a
- Correctness by construction: putting engineering (back) into software (RC), p. 100.
- CASE-2007-ReveliotisR0 #algebra #concurrent #policy #programming #verification
- Correctness Verification of Generalized Algebraic Deadlock Avoidance Policies through Mathematical Programming (SR, ER, JYC), pp. 200–206.
- HPCA-2007-LiY #fault tolerance
- Application-Level Correctness and its Impact on Fault Tolerance (XL, DY), pp. 181–192.
- CSL-2007-NauroisM #exponential #multi #proving
- Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete (PJdN, VM), pp. 435–450.
- ICLP-2007-PettorossiPS #automation #logic programming #program transformation #proving
- Automatic Correctness Proofs for Logic Program Transformations (AP, MP, VS), pp. 364–379.
- LICS-2007-RabinST #performance #proving
- Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications (MOR, RAS, CT), pp. 63–76.
- WCRE-2006-KnieselB #analysis #aspect-oriented #weaving
- An Analysis of the Correctness and Completeness of Aspect Weaving (GK, UB), pp. 324–333.
- CIAA-2006-MesserschmidtMOP #complexity
- Correctness Preservation and Complexity of Simple RL-Automata (HM, FM, FO, MP), pp. 162–172.
- RTA-2006-AntoyBC #on the
- On the Correctness of Bubbling (SA, DWB, SHC), pp. 35–49.
- ICSE-2006-JiangS #c #named #source code #type system #validation
- Osprey: a practical type system for validating dimensional unit correctness of C programs (LJ, ZS), pp. 262–271.
- PPoPP-2006-VafeiadisHHS #proving
- Proving correctness of highly-concurrent linearisable objects (VV, MH, CARH, MS), pp. 129–136.
- SIGMOD-2005-LingaCGS
- Guaranteeing Correctness and Availability in P2P Range Indices (PL, AC, JG, JS), pp. 323–334.
- VLDB-2005-AkalTSBGV #fine-grained #replication #scheduling
- Fine-Grained Replication and Scheduling with Freshness and Correctness Guarantees (FA, CT, HJS, YB, TG, LV), pp. 565–576.
- FM-2005-Gaudel #approximate #formal method #testing
- Formal Methods and Testing: Hypotheses, and Correctness Approximations (MCG), pp. 2–8.
- SEFM-2005-OlssonW #imperative #induction #proving #source code
- Customised Induction Rules for Proving Correctness of Imperative Programs (OO, AW), pp. 180–189.
- SEFM-2005-Trentelman #proving #using
- Proving Correctness of JavaCard DL Taclets using Bali (KT), pp. 160–169.
- ASE-2005-Grov #algorithm #approach #deduction #reasoning #source code #verification
- Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning (GG), pp. 444–447.
- SAC-2005-Lu #declarative #using
- Use of correctness assertions in declarative diagnosis (LL), pp. 1404–1408.
- SAC-2005-WieringaG #coordination #design #process #trust
- Value-oriented design of service coordination processes: correctness and trust (RW, JG), pp. 1320–1327.
- COCV-J-2005-BlechGLM #code generation #comparison #higher-order #optimisation #proving
- Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
- COCV-J-2005-SalcianuA #analysis #data flow #proving
- Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses (AS, KA), pp. 53–68.
- PPoPP-2005-YangBHM #monitoring #source code #trust #verification
- Trust but verify: monitoring remotely executing programs for progress and correctness (SY, ARB, YCH, SPM), pp. 196–205.
- CBSE-2004-KulkarniB #adaptation #component
- Correctness of Component-Based Adaptation (SSK, KNB), pp. 48–58.
- ICFP-2004-ColazzoGMS #query #xml
- Types for path correctness of XML queries (DC, GG, PM, CS), pp. 126–137.
- PEPM-2004-PopeeaC #protocol #proving #type system #verification
- A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.
- POPL-2004-Benton #analysis #program transformation #proving #relational
- Simple relational correctness proofs for static analyses and program transformations (NB), pp. 14–25.
- ICSE-2004-AntoniuSKNF #source code #spreadsheet #validation
- Validating the Unit Correctness of Spreadsheet Programs (TA, PAS, SK, EN, MF), pp. 439–448.
- FoSSaCS-2004-Leivant #logic
- Partial Correctness Assertions Provable in Dynamic Logics (DL), pp. 304–317.
- ITiCSE-2003-Gegg-HarrisonBGOW #contract
- Studying program correctness by constructing contracts (TSGH, GRB, RDG, CMO, JDW), pp. 129–133.
- ITiCSE-2003-Gegg-HarrisonBGOW03a
- Studying program correctness in ProVIDE (TSGH, GRB, RDG, CMO, JDW), p. 262.
- FME-2003-BurdyRL #approach #developer #java
- Java Applet Correctness: A Developer-Oriented Approach (LB, AR, JLL), pp. 422–439.
- FME-2003-DenneyF #policy #safety
- Correctness of Source-Level Safety Policies (ED, BF), pp. 894–913.
- FME-2003-Henderson #proving #using
- Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method (NH), pp. 244–263.
- IFL-2003-SeguraP #analysis #nondeterminism
- Correctness of Non-determinism Analyses in a Parallel-Functional Language (CS, RP), pp. 69–85.
- CHI-2003-WilsonBBGCCDR #programming
- Harnessing curiosity to increase correctness in end-user programming (AW, MMB, LB, OG, LC, CRC, MD, GR), pp. 305–312.
- PLDI-2003-LernerMC #automation #compilation #optimisation #proving
- Automatically proving the correctness of compiler optimizations (SL, TDM, CC), pp. 220–231.
- REFSQ-J-2002-ZowghiG03 #consistency #evolution #on the #requirements
- On the interplay between consistency, completeness, and correctness in requirements evolution (DZ, VG), pp. 993–1009.
- ESOP-2003-ReddyY #data transformation #data type
- Correctness of Data Representations Involving Heap Data Structures (USR, HY), pp. 223–237.
- CBSE-2003-DijkmanAQ #component #process #verification
- Verifying the Correctness of Component-Based Applications that Support Business Processes (RMD, JAA, DAQ), p. 8.
- FME-2002-Hall #development #process
- Correctness by Construction: Integrating Formality into a Commercial Development Process (AH), pp. 224–233.
- FLOPS-2002-Iranzo #on the
- On the Correctness of the Factoring Transformation (PJI), pp. 119–133.
- POPL-2002-LaceyJWF #compilation #logic #optimisation #proving
- Proving correctness of compiler optimizations by temporal logic (DL, NDJ, EVW, CCF), pp. 283–294.
- ICSE-2002-PonsB #development #process #reasoning
- Reasoning about the correctness of software development process (CP, GB), p. 708.
- SAC-2002-FerriPR #database #query #semantics
- The syntactic and semantic correctness of pictorial configurations to query geographic databases by PQL (FF, EP, MR), pp. 432–437.
- FoSSaCS-2002-BoerGM #concurrent #constraints #proving #source code
- Proving Correctness of Timed Concurrent Constraint Programs (FSdB, MG, MCM), pp. 37–51.
- FME-2001-StoySA #protocol #proving
- Proofs of Correctness of Cache-Coherence Protocols (JES, XS, A), pp. 43–71.
- IFL-2001-ButterfieldS #comparison #paradigm #proving #source code
- Proving Correctness of Programs with IO — A Paradigm Comparison (AB, GS), pp. 72–87.
- IFL-2001-EncinaP #proving
- Proving the Correctness of the STG Machine (AdlE, RP), pp. 88–104.
- SEKE-2001-BarberGH #architecture #model checking #simulation #using
- Evaluating Dynamic Correctness Properties of Domain Reference Architectures Using a Combination of Simulation and Model Checking (KSB, TJG, JH), pp. 19–28.
- POPL-2001-Calcagno #calculus #safety #semantics
- Stratified operational semantics for safety and correctness of the region calculus (CC), pp. 155–165.
- CSL-2001-Mogbil #commutative #logic #polynomial
- Quadratic Correctness Criterion for Non-commutative Logic (VM), pp. 69–83.
- ICLP-2001-DrabentM #approach #declarative #proving #source code
- Proving Correctness and Completeness of Normal Programs — A Declarative Approach (WD, MM), pp. 284–299.
- LICS-2001-KozenT #linear #logic
- Intuitionistic Linear Logic and Partial Correctness (DK, JT), pp. 259–268.
- ICSM-2000-GibsonDM #maintenance
- The Application of Correctness Preserving Transformations to Software Maintenance (JPG, TFD, BAM), p. 108–?.
- SAIG-2000-FischbachH #specification
- Specification and Correctness of λ Lifting (AF, JH), pp. 108–128.
- ESOP-2000-DenneyJ #java #logic
- Correctness of Java Card Method Lookup via Logical Relations (ED, TPJ), pp. 104–118.
- ESOP-2000-Hughes
- The Correctness of Type Specialisation (JH), pp. 215–229.
- WICSA-1999-Riemenschneider #architecture
- Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures (RAR), pp. 65–82.
- PODS-1999-AlonsoFPS #component #transaction
- Correctness in General Configurations of Transactional Components (GA, AF, GP, HJS), pp. 285–293.
- FM-v1-1999-MoninK #algorithm #consistency #proving #standard
- Correctness Proof of the Standardized Algorithm for ABR Conformance (JFM, FK), pp. 662–681.
- LICS-1999-Guerrini #linear #multi #proving
- Correctness of Multiplicative Proof Nets Is Linear (SG), pp. 454–463.
- FM-1998-GoerigkH #compilation #how #implementation
- Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct (WG, UH), pp. 122–136.
- ECOOP-1998-FerreiraS #algorithm #distributed #garbage collection #modelling #proving
- Modelling a Distributed Cached Store for Garbage Collection: The Algorithm and Its Correctness Proof (PF, MS), pp. 234–259.
- POPL-1998-AriolaS #calculus #call-by #imperative #monad
- Correctness of Monadic State: An Imperative Call-by-Need Calculus (ZMA, AS), pp. 62–74.
- POPL-1998-Blanchet #analysis #implementation #proving
- Escape Analysis: Correctness Proof, Implementation and Experimental Results (BB), pp. 25–37.
- SAS-1998-HillBZ
- The Correctness of Set-Sharing (PMH, RB, EZ), pp. 99–114.
- CAV-1998-Balarin #approach #concurrent #modelling #verification
- Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models (FB), pp. 391–402.
- CAV-1998-HosabettuSG #pipes and filters #proving
- Decomposing the Proof of Correctness of pipelined Microprocessors (RH, MKS, GG), pp. 122–134.
- PODS-1997-AlonsoBFS #parallel
- Correctness and Parallelism of Composite Systems (GA, SB, AF, HJS), pp. 197–208.
- EDTC-1997-EisenbieglerKB #approach #towards
- A constructive approach towards correctness of synthesis-application within retiming (DE, RK, CB), pp. 427–431.
- TAPSOFT-1997-Jacobs #algebra #behaviour #induction #proving #specification
- Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs (BJ0), pp. 787–802.
- TAPSOFT-1997-ReifSS #proving
- Proving System Correctness with KIV (WR, GS, KS), pp. 859–862.
- CADE-1997-ReifSS #proving
- Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.
- POPL-1996-HughesPS #proving #using
- Proving the Correctness of Reactive Systems Using Sized Types (JH, LP, AS), pp. 410–423.
- SAS-1996-BoerGP #constraints #logic programming #proving #scheduling #source code
- Proving Correctness of Constraint Logic Programs with Dynamic Scheduling (FSdB, MG, CP), pp. 83–97.
- DAC-1996-KantrowitzN #analysis #simulation #verification #what
- I’m Done Simulating: Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor (MK, LMN), pp. 325–330.
- TAPSOFT-J-1995-Sands96 #automation #program transformation #proving #recursion
- Proving the Correctness of Recursion-Based Automatic Program Transformations (DS), pp. 193–233.
- LICS-1996-AlurMP #concurrent #model checking
- Model-Checking of Correctness Conditions for Concurrent Objects (RA, KLM, DP), pp. 219–228.
- SIGMOD-1995-HouZ #approach #database #statistics
- Enhancing Database Correctness: a Statistical Approach (WCH, ZZ), pp. 223–232.
- FPCA-1995-Wand #compilation #parallel
- Compiler Correctness for Parallel Languages (MW), pp. 120–134.
- SEKE-1995-BernardeschiFP #architecture #interactive #specification #user interface
- Application of Correctness Preserving Transformations for Deriving Architectural Descriptions of Interactive Systems from User Interface Specifications (CB, AF, FP), pp. 234–243.
- PLILP-1995-Hatcliff #verification
- Mechanically Verifying the Correctness of an Offline Partial Evaluator (JH), pp. 279–298.
- POPL-1995-Sands #program transformation
- Total Correctness by Local Improvement in Program Transformation (DS), pp. 221–232.
- PDP-1995-MendivilDBG #algorithm #concurrent #distributed
- Correctness of a distributed deadlock resolution algorithm for the single request model (JRGdM, AD, JMBA, JRG), pp. 254–261.
- TAPSOFT-1995-Sands #automation #program transformation #proving #recursion
- Proving the Correctness of Recursion-Based Automatic Program Transformations (DS), pp. 681–695.
- ICLP-1995-Hirata #haskell #proving #π-calculus
- Proving Correctness of Translation from Moded Flat GHC to π-Calculus (KH), p. 818.
- ILPS-1995-FerrandL #composition #logic programming #proving #source code
- A Compositional Proof Method of Partial Correctness for Normal Logic Programs (GF, AL), pp. 209–223.
- ILPS-1995-LauOPP #logic programming #program transformation #termination
- Correctness of Logic Program Transformations Based on Existential Termination (KKL, MO, AP, MP), pp. 480–494.
- ICALP-1994-VergauwenL #equation #performance
- Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems (BV, JL), pp. 304–315.
- POPL-1994-Ramsey #implementation
- Correctness of Trap-Based Breakpoint Implementations (NR), pp. 15–24.
- FSE-1994-MoriconiQ #architecture #composition
- Correctness and Composition of Software Architectures (MM, XQ), pp. 164–174.
- CC-1994-LammelR #prototype
- Provable Correctness of Prototype Interpreters in LDL (RL, GR), pp. 218–232.
- ISSTA-1994-Marcus #composition #testing #verification
- The Incorporation of Testing into Verification: Direct, Modular, and Hierarchical Correctness Degrees (LM), p. 197.
- PODS-1993-RastogiMBKS #on the
- On Correctness of Non-serializable Executions (RR, SM, YB, HFK, AS), pp. 97–108.
- RTA-1993-ChakrabartiY #algorithm #distributed #memory management #on the
- On the Correctness of a Distributed Memory Gröbner basis Algorithm (SC, KAY), pp. 77–91.
- PEPM-1993-Lange #code generation
- The Correctness of an Optimized Code Generation (TPL), pp. 167–178.
- PLILP-1993-BurnM #analysis #compilation #optimisation #proving #strict
- Proving the Correctness of Compiler Optimizations Based on Strictness Analysis (GLB, DLM), pp. 346–364.
- POPL-1993-Wand #analysis #specification
- Specifying the Correctness of Binding-Time Analysis (MW), pp. 137–143.
- WSA-1993-BruynoogheC
- Freeness, Sharing, Linearity and Correctness — All at Once (MB, MC), pp. 153–164.
- ICSE-1993-BastaniDP #evaluation #using
- Experimental Evaluation of a Fuzzy-Set Based Measure of Software Correctness Using Program Mutation (FBB, GD, AP), pp. 45–54.
- ICLP-1993-CodishDFB #analysis #logic programming #question #source code
- Freeness Analysis for Logic Programs — And Correctness? (MC, DD, GF, MB), pp. 116–131.
- LFP-1992-WandO #proving
- Proving the Correctness of Storage Representations (MW, DO), pp. 151–160.
- SEKE-1992-Reif #first-order #specification
- Correctness of Full First-Order Specifications (WR), pp. 276–283.
- TOOLS-USA-1992-Weber #how
- Getting Class Correctness and System Correctness Equivalent (How to get covariance right) (FW), pp. 199–213.
- STOC-1992-AttiyaF #multi
- A Correctness Condition for High-Performance Multiprocessors (HA, RF), pp. 679–690.
- CADE-1992-BoyerY #automation #proving #source code
- Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (RSB, YY), pp. 416–430.
- CAV-1992-Larsen #performance
- Efficient Local Correctness Checking (KGL), pp. 30–43.
- JICSLP-1992-FerrandD #logic programming #proving #source code
- Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs (GF, PD), pp. 161–174.
- ML-1991-VanLehnJ #learning #physics
- Learning Physics Via Explanation-Based Learning of Correctness and Analogical Search Control (KV, RMJ), pp. 110–114.
- PEPM-1991-McNerney #abstract interpretation #compilation #using #verification
- Verifying the Correctness of Compiler Transformations on Basic Blocks using Abstract Interpretation (TSM), pp. 106–115.
- CCPSD-1991-Burn #evaluation #reduction
- The Evaluation Transformer Model of Reduction and Its Correctness (GLB), pp. 458–482.
- CAV-1991-Mutz #behaviour #proving #term rewriting #using
- Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior (MM), pp. 277–287.
- CSL-1991-BeierleB #proving
- Correctness Proof For the WAM with Types (CB, EB), pp. 15–34.
- ICLP-1991-ColussiM #axiom #logic programming #proving #semantics #source code #using
- Proving Correctness of Logic Programs Using Axiomatic Semantics (LC, EM), pp. 629–642.
- ICALP-1990-Schwartzbach
- Static Correctness of Hierarchical Procedures (MIS), pp. 32–45.
- VDME-1990-HaastrupG #in the small
- Correctness in the Small (PH, CG), pp. 72–98.
- ALP-1990-Farres-Casals #proving #specification
- Proving Correctness wrt Specifications with Hidden Parts (JFC), pp. 25–39.
- PLILP-1990-BoeckC #analysis #prolog #static typing
- Static Type Analysis of Prolog Procedures for Ensuring Correctness (PDB, BLC), pp. 222–237.
- POPL-1990-Gunter #nondeterminism #source code
- Relating Total and Partial Correctness Interpretations of Non-Deterministic Programs (CAG), pp. 306–319.
- SIGMOD-1989-MarkowitzS #on the #relational #representation
- On the Correctness of Representing Extended Entity-Relationship Structures in the Relational Model (VMM, AS), pp. 430–439.
- VLDB-1989-DuE #concurrent
- Quasi Serializability: a Correctness Criterion for Global Concurrency Control in InterBase (WD, AKE), pp. 347–355.
- OOPSLA-1989-CookP #inheritance #semantics
- A Denotational Semantics of Inheritance and its Correctness (WRC, JP), pp. 433–443.
- CCIPL-1989-BossiC #logic programming #source code #verification
- Verifying Correctness of Logic Programs (AB, NC), pp. 96–110.
- NACLP-1989-HermenegildoR #independence #logic programming #on the #performance #source code
- On the Correctness and Efficiency of Independent And-Parallelism in Logic Programs (MVH, FR), pp. 369–389.
- TAV-1989-RosenblumL #specification #testing
- Testing the Correctness of Tasking Supervisors with TSL Specifications (DSR, DCL), pp. 187–196.
- SIGMOD-1988-KorthS #formal method
- Formal Model of Correctness Without Serializability (HFK, GDS), pp. 379–386.
- VDME-1988-ButhB #code generation #proving #specification #term rewriting #using
- Correctness Proofs for Meta IV Written Code Generator Specification using Term Rewriting (BB, KHB), pp. 406–433.
- VDME-1988-Naftalin
- Correctness for Beginners (MN), pp. 26–47.
- DAC-1988-MadreB #behaviour #comparison #proving #using
- Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour (JCM, JPB), pp. 205–210.
- LICS-1988-HoareG #logic
- Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic (CARH, MJCG), pp. 28–36.
- CAAP-1987-NavarroO #horn clause #proving #specification
- Parameterized Horn Clause Specifications: Proof Theory and Correctness (MN, FO), pp. 202–216.
- ICALP-1986-Stirling #composition #concurrent #logic
- A Compositional Reformulation of Owicki-Gries’s Partial Correctness Logic for a Concurrent While Language (CS), pp. 407–415.
- ESOP-1986-Nielson #code generation #metalanguage
- Correctness of Code Generation from a Two-Level Meta-Language (FN), pp. 30–40.
- LICS-1986-Brookes #concurrent #csp #proving #semantics
- A Semantically Based Proof System for Partial Correctness and Deadlock in CSP (SDB), pp. 58–65.
- LICS-1986-Csirmaz #finite
- Program Correctness on Finite Fields (LC, BH), pp. 4–10.
- PODS-1985-CasanovaMT #on the
- On the Correctness of a Local Storage Subsystem (MAC, AVM, LT), pp. 123–134.
- PODS-1985-TuzhilinS #approach #concurrent #semantics #transaction
- A Semantic Approach to Correctness of Concurrent Transaction Executions (AT, PGS), pp. 85–95.
- ICSE-1984-Chyou #proving
- Structure Charts and Program Correctness Proofs (SCC), pp. 486–498.
- POPL-1982-GansnerHKMS #query #semantics
- Semantics and Correctness of a Query Language Translation (EG, JRH, CMRK, DJM, PS), pp. 289–298.
- DAC-1982-Leinwand #logic
- Logical correctness by construction (SML), pp. 825–831.
- PS-1981-ColemanG #distributed #source code
- Partial Correctness of Distributed Programs (DC, RMG), pp. 138–180.
- DAC-1981-McFarland #automation #design #on the #optimisation #proving
- On proving the correctness of optimizing transformations in a digital design automation system (MCM), pp. 90–97.
- STOC-1981-Yannakakis #concurrent #database
- Issues of Correctness in Database Concurrency Control by Locking (MY), pp. 363–367.
- ICALP-1980-EhrigKP #algebra #concept #data type #implementation #semantics #syntax
- Algebraic Implementation of Abstract Data Types: Concept, Syntax, Semantics and Correctness (HE, HJK, PP), pp. 142–156.
- ICALP-1980-EmersonC #fixpoint #parallel #source code #using
- Characterizing Correctness Properties of Parallel Programs Using Fixpoints (EAE, EMC), pp. 169–181.
- ICALP-1980-Mosses #approach #compilation
- A Constructive Approach to Compiler Correctness (PDM), pp. 449–469.
- POPL-1980-BuddDLS #functional #source code #using
- Theoretical and Emperical Studies on Using Program Mutation to Test the Functional Correctness of Programs (TAB, RAD, RJL, FGS), pp. 220–233.
- DAC-1980-CoryC #design #verification
- Developments in verification of design correctness (WEC, WMvC), pp. 156–164.
- SDCG-1980-Mosses #approach #compilation
- A constructive approach to compiler correctness (PDM), pp. 189–210.
- CADE-1980-Gloess #empirical #parsing #proving #theorem proving
- An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
- ICALP-1979-DuncanY #algorithm #proving
- Studies in Abstract/Concrete Mappings in Proving Algorithm Correctness (AGD, LY), pp. 218–229.
- FM-1979-BergFM #overview #perspective
- Correctness of Software — An Overview (HKB, WRF, TGM), pp. 237–354.
- ICALP-1978-Gallier #nondeterminism #recursion #semantics #source code
- Semantics and Correctness of Nondeterministic Flowchart Programs with Recursive Procedures (JHG), pp. 251–267.
- POPL-1977-Doeppner #parallel #refinement
- Parallel Program Correctness Through Refinement (TWDJ), pp. 155–169.
- SOSP-1977-Ellis #consistency #database
- Consistency and Correctness of Duplicate Database Systems (CAE), pp. 67–84.
- POPL-1976-Geller #proving #testing
- Test Data as an Aid in Proving Program Correctness (MMG), pp. 209–218.
- ICSE-1976-Gries #proving #source code
- An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs (DG), p. 200.
- ICSE-1976-MannaW #proving
- Is “Sometime” Sometimes Better Than “Always”? Intermittent Assertions in Proving Program Correctness (ZM, RJW), pp. 32–39.
- SIGFIDET-1972-HawryszkiewyczD #approach #database #proving
- An Approach to Proving the Correctness of Data Base Operations (IH, JBD), pp. 323–348.
- SOSP-1971-Kahn #approach
- An Approach to System Correctness (GK), pp. 86–94.
- STOC-1970-McGowan
- The Correctness of a Modified SECD Machine (CLM), pp. 149–157.