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.