callback( { "result":{ "query":":facetid:toc:\"db/conf/cav/cav2004.bht\"", "status":{ "@code":"200", "text":"OK" }, "time":{ "@unit":"msecs", "text":"68.32" }, "completions":{ "@total":"1", "@computed":"1", "@sent":"1", "c":{ "@sc":"52", "@dc":"52", "@oc":"52", "@id":"43383251", "text":":facetid:toc:db/conf/cav/cav2004.bht" } }, "hits":{ "@total":"52", "@computed":"52", "@sent":"30", "@first":"0", "hit":[{ "@score":"1", "@id":"6023182", "info":{"authors":{"author":[{"@pid":"a/PAAbdulla","text":"Parosh Aziz Abdulla"},{"@pid":"j/BengtJonsson","text":"Bengt Jonsson 0001"},{"@pid":"05/1762","text":"Marcus Nilsson"},{"@pid":"74/215","text":"Julien d'Orso"},{"@pid":"26/1444","text":"Mayank Saksena"}]},"title":"Regular Model Checking for LTL(MSO).","venue":"CAV","pages":"348-360","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/AbdullaJNdS04","doi":"10.1007/978-3-540-27813-9_27","ee":"https://doi.org/10.1007/978-3-540-27813-9_27","url":"https://dblp.org/rec/conf/cav/AbdullaJNdS04"}, "url":"URL#6023182" }, { "@score":"1", "@id":"6023183", "info":{"authors":{"author":[{"@pid":"04/4098","text":"Tony Andrews"},{"@pid":"q/ShazQadeer","text":"Shaz Qadeer"},{"@pid":"r/SriramKRajamani","text":"Sriram K. Rajamani"},{"@pid":"r/JakobRehof","text":"Jakob Rehof"},{"@pid":"x/YichenXie","text":"Yichen Xie 0001"}]},"title":"Zing: A Model Checker for Concurrent Software.","venue":"CAV","pages":"484-487","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/AndrewsQRRX04","doi":"10.1007/978-3-540-27813-9_42","ee":"https://doi.org/10.1007/978-3-540-27813-9_42","url":"https://dblp.org/rec/conf/cav/AndrewsQRRX04"}, "url":"URL#6023183" }, { "@score":"1", "@id":"6023184", "info":{"authors":{"author":{"@pid":"73/832","text":"Tamarah Arons"}},"title":"Verification of an Advanced mips-Type Out-of-Order Execution Algorithm.","venue":"CAV","pages":"414-426","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/Arons04","doi":"10.1007/978-3-540-27813-9_32","ee":"https://doi.org/10.1007/978-3-540-27813-9_32","url":"https://dblp.org/rec/conf/cav/Arons04"}, "url":"URL#6023184" }, { "@score":"1", "@id":"6023185", "info":{"authors":{"author":[{"@pid":"21/6330","text":"Cyrille Artho"},{"@pid":"s/ViktorSchuppan","text":"Viktor Schuppan"},{"@pid":"b/ArminBiere","text":"Armin Biere"},{"@pid":"98/5806","text":"Pascal Eugster"},{"@pid":"50/3025","text":"Marcel Baur"},{"@pid":"75/1560","text":"Boris Zweimüller"}]},"title":"JNuke: Efficient Dynamic Analysis for Java.","venue":"CAV","pages":"462-465","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/ArthoSBEBZ04","doi":"10.1007/978-3-540-27813-9_37","ee":"https://doi.org/10.1007/978-3-540-27813-9_37","url":"https://dblp.org/rec/conf/cav/ArthoSBEBZ04"}, "url":"URL#6023185" }, { "@score":"1", "@id":"6023186", "info":{"authors":{"author":[{"@pid":"12/389","text":"Mohammad Awedh"},{"@pid":"62/5300","text":"Fabio Somenzi"}]},"title":"Proving More Properties with Bounded Model Checking.","venue":"CAV","pages":"96-108","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/AwedhS04","doi":"10.1007/978-3-540-27813-9_8","ee":"https://doi.org/10.1007/978-3-540-27813-9_8","url":"https://dblp.org/rec/conf/cav/AwedhS04"}, "url":"URL#6023186" }, { "@score":"1", "@id":"6023187", "info":{"authors":{"author":[{"@pid":"b/ThomasBall","text":"Thomas Ball"},{"@pid":"36/113","text":"Byron Cook"},{"@pid":"32/2903","text":"Shuvendu K. Lahiri"},{"@pid":"94/5689","text":"Lintao Zhang"}]},"title":"Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.","venue":"CAV","pages":"457-461","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BallCLZ04","doi":"10.1007/978-3-540-27813-9_36","ee":"https://doi.org/10.1007/978-3-540-27813-9_36","url":"https://dblp.org/rec/conf/cav/BallCLZ04"}, "url":"URL#6023187" }, { "@score":"1", "@id":"6023188", "info":{"authors":{"author":[{"@pid":"b/ClarkWBarrett","text":"Clark W. Barrett"},{"@pid":"05/2504","text":"Sergey Berezin"}]},"title":"CVC Lite: A New Implementation of the Cooperating Validity Checker Category B.","venue":"CAV","pages":"515-518","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BarrettB04","doi":"10.1007/978-3-540-27813-9_49","ee":"https://doi.org/10.1007/978-3-540-27813-9_49","url":"https://dblp.org/rec/conf/cav/BarrettB04"}, "url":"URL#6023188" }, { "@score":"1", "@id":"6023189", "info":{"authors":{"author":[{"@pid":"48/1067","text":"Constantinos Bartzis"},{"@pid":"07/3368","text":"Tevfik Bultan"}]},"title":"Widening Arithmetic Automata.","venue":"CAV","pages":"321-333","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BartzisB04","doi":"10.1007/978-3-540-27813-9_25","ee":"https://doi.org/10.1007/978-3-540-27813-9_25","url":"https://dblp.org/rec/conf/cav/BartzisB04"}, "url":"URL#6023189" }, { "@score":"1", "@id":"6023190", "info":{"authors":{"author":[{"@pid":"07/4415","text":"Jesse D. Bingham"},{"@pid":"c/AnneCondon","text":"Anne Condon"},{"@pid":"01/2712","text":"Alan J. Hu"},{"@pid":"q/ShazQadeer","text":"Shaz Qadeer"},{"@pid":"14/1166","text":"Zhichuan Zhang"}]},"title":"Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values.","venue":"CAV","pages":"427-439","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BinghamCHQZ04","doi":"10.1007/978-3-540-27813-9_33","ee":"https://doi.org/10.1007/978-3-540-27813-9_33","url":"https://dblp.org/rec/conf/cav/BinghamCHQZ04"}, "url":"URL#6023190" }, { "@score":"1", "@id":"6023191", "info":{"authors":{"author":[{"@pid":"b/AhmedBouajjani","text":"Ahmed Bouajjani"},{"@pid":"22/639","text":"Peter Habermehl"},{"@pid":"51/533","text":"Tomás Vojnar"}]},"title":"Abstract Regular Model Checking.","venue":"CAV","pages":"372-386","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BouajjaniHV04","doi":"10.1007/978-3-540-27813-9_29","ee":"https://doi.org/10.1007/978-3-540-27813-9_29","url":"https://dblp.org/rec/conf/cav/BouajjaniHV04"}, "url":"URL#6023191" }, { "@score":"1", "@id":"6023192", "info":{"authors":{"author":[{"@pid":"b/VictorABraberman","text":"Víctor A. Braberman"},{"@pid":"g/DiegoGarbervetsky","text":"Diego Garbervetsky"},{"@pid":"67/578","text":"Alfredo Olivero"}]},"title":"ObsSlice: A Timed Automata Slicer Based on Observers.","venue":"CAV","pages":"470-474","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BrabermanGO04","doi":"10.1007/978-3-540-27813-9_39","ee":"https://doi.org/10.1007/978-3-540-27813-9_39","url":"https://dblp.org/rec/conf/cav/BrabermanGO04"}, "url":"URL#6023192" }, { "@score":"1", "@id":"6023193", "info":{"authors":{"author":[{"@pid":"30/5512","text":"Doron Bustan"},{"@pid":"07/1731","text":"Sasha Rubin"},{"@pid":"v/MosheYVardi","text":"Moshe Y. Vardi"}]},"title":"Verifying omega-Regular Properties of Markov Chains.","venue":"CAV","pages":"189-201","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/BustanRV04","doi":"10.1007/978-3-540-27813-9_15","ee":"https://doi.org/10.1007/978-3-540-27813-9_15","url":"https://dblp.org/rec/conf/cav/BustanRV04"}, "url":"URL#6023193" }, { "@score":"1", "@id":"6023194", "info":{"authors":{"author":[{"@pid":"15/947","text":"Jacob Chang"},{"@pid":"05/2504","text":"Sergey Berezin"},{"@pid":"d/DavidLDill","text":"David L. Dill"}]},"title":"Using Interface Refinement to Integrate Formal Verification into the Design Cycle.","venue":"CAV","pages":"122-134","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/ChangBD04","doi":"10.1007/978-3-540-27813-9_10","ee":"https://doi.org/10.1007/978-3-540-27813-9_10","url":"https://dblp.org/rec/conf/cav/ChangBD04"}, "url":"URL#6023194" }, { "@score":"1", "@id":"6023195", "info":{"authors":{"author":[{"@pid":"89/148","text":"Azadeh Farzan"},{"@pid":"21/3047-6","text":"Feng Chen 0006"},{"@pid":"m/JoseMeseguer","text":"José Meseguer 0001"},{"@pid":"r/GrigoreRosu","text":"Grigore Rosu"}]},"title":"Formal Analysis of Java Programs in JavaFAN.","venue":"CAV","pages":"501-505","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/FarzanCMR04","doi":"10.1007/978-3-540-27813-9_46","ee":"https://doi.org/10.1007/978-3-540-27813-9_46","url":"https://dblp.org/rec/conf/cav/FarzanCMR04"}, "url":"URL#6023195" }, { "@score":"1", "@id":"6023196", "info":{"authors":{"author":[{"@pid":"f/AlainFinkel","text":"Alain Finkel"},{"@pid":"50/3164","text":"Jérôme Leroux"}]},"title":"Image Computation in Infinite State Model Checking.","venue":"CAV","pages":"361-371","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/FinkelL04","doi":"10.1007/978-3-540-27813-9_28","ee":"https://doi.org/10.1007/978-3-540-27813-9_28","url":"https://dblp.org/rec/conf/cav/FinkelL04"}, "url":"URL#6023196" }, { "@score":"1", "@id":"6023197", "info":{"authors":{"author":[{"@pid":"f/CedricFournet","text":"Cédric Fournet"},{"@pid":"h/CARHoare","text":"C. A. R. Hoare"},{"@pid":"r/SriramKRajamani","text":"Sriram K. Rajamani"},{"@pid":"r/JakobRehof","text":"Jakob Rehof"}]},"title":"Stuck-Free Conformance.","venue":"CAV","pages":"242-254","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/FournetHRR04","doi":"10.1007/978-3-540-27813-9_19","ee":"https://doi.org/10.1007/978-3-540-27813-9_19","url":"https://dblp.org/rec/conf/cav/FournetHRR04"}, "url":"URL#6023197" }, { "@score":"1", "@id":"6023198", "info":{"authors":{"author":[{"@pid":"97/374-1","text":"Xiang Fu 0001"},{"@pid":"07/3368","text":"Tevfik Bultan"},{"@pid":"s/JWSu","text":"Jianwen Su"}]},"title":"WSAT: A Tool for Formal Analysis of Web Services.","venue":"CAV","pages":"510-514","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/FuBS04","doi":"10.1007/978-3-540-27813-9_48","ee":"https://doi.org/10.1007/978-3-540-27813-9_48","url":"https://dblp.org/rec/conf/cav/FuBS04"}, "url":"URL#6023198" }, { "@score":"1", "@id":"6023199", "info":{"authors":{"author":[{"@pid":"20/6956","text":"Peter Gammie"},{"@pid":"m/RvdMeyden","text":"Ron van der Meyden"}]},"title":"MCK: Model Checking the Logic of Knowledge.","venue":"CAV","pages":"479-483","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GammieM04","doi":"10.1007/978-3-540-27813-9_41","ee":"https://doi.org/10.1007/978-3-540-27813-9_41","url":"https://dblp.org/rec/conf/cav/GammieM04"}, "url":"URL#6023199" }, { "@score":"1", "@id":"6023200", "info":{"authors":{"author":[{"@pid":"34/7032","text":"Malay K. Ganai"},{"@pid":"18/2229","text":"Aarti Gupta"},{"@pid":"18/2806","text":"Pranav Ashar"}]},"title":"Efficient Modeling of Embedded Memories in Bounded Model Checking.","venue":"CAV","pages":"440-452","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GanaiGA04","doi":"10.1007/978-3-540-27813-9_34","ee":"https://doi.org/10.1007/978-3-540-27813-9_34","url":"https://dblp.org/rec/conf/cav/GanaiGA04"}, "url":"URL#6023200" }, { "@score":"1", "@id":"6023201", "info":{"authors":{"author":[{"@pid":"g/HaraldGanzinger","text":"Harald Ganzinger"},{"@pid":"51/1978","text":"George Hagen"},{"@pid":"n/RobertNieuwenhuis","text":"Robert Nieuwenhuis"},{"@pid":"99/5829","text":"Albert Oliveras"},{"@pid":"37/4921","text":"Cesare Tinelli"}]},"title":"DPLL( T): Fast Decision Procedures.","venue":"CAV","pages":"175-188","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GanzingerHNOT04","doi":"10.1007/978-3-540-27813-9_14","ee":"https://doi.org/10.1007/978-3-540-27813-9_14","url":"https://dblp.org/rec/conf/cav/GanzingerHNOT04"}, "url":"URL#6023201" }, { "@score":"1", "@id":"6023202", "info":{"authors":{"author":[{"@pid":"46/5223","text":"Hui Gao"},{"@pid":"h/WimHHesselink","text":"Wim H. Hesselink"}]},"title":"A Formal Reduction for Lock-Free Parallel Algorithms.","venue":"CAV","pages":"44-56","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GaoH04","doi":"10.1007/978-3-540-27813-9_4","ee":"https://doi.org/10.1007/978-3-540-27813-9_4","url":"https://dblp.org/rec/conf/cav/GaoH04"}, "url":"URL#6023202" }, { "@score":"1", "@id":"6023203", "info":{"authors":{"author":[{"@pid":"68/6702","text":"Amit Goel"},{"@pid":"b/REBryant","text":"Randal E. Bryant"}]},"title":"Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors.","venue":"CAV","pages":"255-267","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GoelB04","doi":"10.1007/978-3-540-27813-9_20","ee":"https://doi.org/10.1007/978-3-540-27813-9_20","url":"https://dblp.org/rec/conf/cav/GoelB04"}, "url":"URL#6023203" }, { "@score":"1", "@id":"6023204", "info":{"authors":{"author":[{"@pid":"g/GGopalakrishnan","text":"Ganesh Gopalakrishnan"},{"@pid":"54/6179","text":"Yue Yang"},{"@pid":"91/4476","text":"Hemanthkumar Sivaraj"}]},"title":"QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings.","venue":"CAV","pages":"401-413","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GopalakrishnanYS04","doi":"10.1007/978-3-540-27813-9_31","ee":"https://doi.org/10.1007/978-3-540-27813-9_31","url":"https://dblp.org/rec/conf/cav/GopalakrishnanYS04"}, "url":"URL#6023204" }, { "@score":"1", "@id":"6023205", "info":{"authors":{"author":[{"@pid":"39/6111","text":"Alain Griffault"},{"@pid":"99/5314","text":"Aymeric Vincent"}]},"title":"The Mec 5 Model-Checker.","venue":"CAV","pages":"488-491","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GriffaultV04","doi":"10.1007/978-3-540-27813-9_43","ee":"https://doi.org/10.1007/978-3-540-27813-9_43","url":"https://dblp.org/rec/conf/cav/GriffaultV04"}, "url":"URL#6023205" }, { "@score":"1", "@id":"6023206", "info":{"authors":{"author":[{"@pid":"g/AlexGroce","text":"Alex Groce"},{"@pid":"k/DanielKroening","text":"Daniel Kroening"},{"@pid":"38/6631","text":"Flavio Lerda"}]},"title":"Understanding Counterexamples with explain.","venue":"CAV","pages":"453-456","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/GroceKL04","doi":"10.1007/978-3-540-27813-9_35","ee":"https://doi.org/10.1007/978-3-540-27813-9_35","url":"https://dblp.org/rec/conf/cav/GroceKL04"}, "url":"URL#6023206" }, { "@score":"1", "@id":"6023207", "info":{"authors":{"author":{"@pid":"38/356","text":"Warren A. Hunt Jr."}},"title":"Mechanical Mathematical Methods for Microprocessor Verification.","venue":"CAV","pages":"523-533","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/Hunt04","doi":"10.1007/978-3-540-27813-9_51","ee":"https://doi.org/10.1007/978-3-540-27813-9_51","url":"https://dblp.org/rec/conf/cav/Hunt04"}, "url":"URL#6023207" }, { "@score":"1", "@id":"6023208", "info":{"authors":{"author":[{"@pid":"i/NeilImmerman","text":"Neil Immerman"},{"@pid":"r/AlexanderMosheRabinovich","text":"Alexander Moshe Rabinovich"},{"@pid":"r/TWReps","text":"Thomas W. Reps"},{"@pid":"s/SSagiv","text":"Shmuel Sagiv"},{"@pid":"50/6710","text":"Greta Yorsh"}]},"title":"Verification via Structure Simulation.","venue":"CAV","pages":"281-294","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/ImmermanRRSY04","doi":"10.1007/978-3-540-27813-9_22","ee":"https://doi.org/10.1007/978-3-540-27813-9_22","url":"https://dblp.org/rec/conf/cav/ImmermanRRSY04"}, "url":"URL#6023208" }, { "@score":"1", "@id":"6023209", "info":{"authors":{"author":[{"@pid":"13/2622","text":"Jie-Hong Roland Jiang"},{"@pid":"b/RobertKBrayton","text":"Robert K. Brayton"}]},"title":"Functional Dependency for Verification Reduction.","venue":"CAV","pages":"268-280","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/JiangB04","doi":"10.1007/978-3-540-27813-9_21","ee":"https://doi.org/10.1007/978-3-540-27813-9_21","url":"https://dblp.org/rec/conf/cav/JiangB04"}, "url":"URL#6023209" }, { "@score":"1", "@id":"6023210", "info":{"authors":{"author":[{"@pid":"12/2963","text":"HoonSang Jin"},{"@pid":"12/389","text":"Mohammad Awedh"},{"@pid":"62/5300","text":"Fabio Somenzi"}]},"title":"CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking.","venue":"CAV","pages":"519-522","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/JinAS04","doi":"10.1007/978-3-540-27813-9_50","ee":"https://doi.org/10.1007/978-3-540-27813-9_50","url":"https://dblp.org/rec/conf/cav/JinAS04"}, "url":"URL#6023210" }, { "@score":"1", "@id":"6023211", "info":{"authors":{"author":[{"@pid":"k/DanielKroening","text":"Daniel Kroening"},{"@pid":"55/4663","text":"Joël Ouaknine"},{"@pid":"s/SanjitASeshia","text":"Sanjit A. Seshia"},{"@pid":"s/OferStrichman","text":"Ofer Strichman"}]},"title":"Abstraction-Based Satisfiability Solving of Presburger Arithmetic.","venue":"CAV","pages":"308-320","year":"2004","type":"Conference and Workshop Papers","access":"closed","key":"conf/cav/KroeningOSS04","doi":"10.1007/978-3-540-27813-9_24","ee":"https://doi.org/10.1007/978-3-540-27813-9_24","url":"https://dblp.org/rec/conf/cav/KroeningOSS04"}, "url":"URL#6023211" } ] } } } )