For all the literatures I have seen, modular reasoning for object-oriented programs is only concerned on the source code level. I'm wondering is this because we don't need modularity at low-level code, or compared to other verification challenges of bytecode, modular reasoning is, to some extent, too far away from applications? Most modular reasoning methodologies are based on Liskov's behavioral subtyping( or its extensions), while sometimes it is too concrete for OO programs. What I wanna to do is using Parkinson's APF to verify source program(java, for example), and then translated into bytecode proof. On the level of method call, proof obligation of APF is preserved by non-optimized complilers. But I still need to prove that, and think more about the significance of modular reasoning on bytecode.
来源于 :)OXFORDUNIVERSITY COMPUTINGLABORATORY Verification The verification group at Oxford is internationally recognized as among the largest and strongest in the world. Our work spans a wide range of research, from fundamental investigations into the decidability and complexity of model checking for various types of infinite-state systems, through process calculi, logics and semantic models, all the way to practical, machine-assisted methods applicable to real-world problems and programming languages. We also have strong industrial links. Our key strengths include concurrency, abstraction, industrial-scale hardware verification, software model checking, and verification of real-time and probabilistic systems, with applications in security protocols, power management, nanotechnology, and biology. A major source of impact is the adoption by others of verification tools resulting from our research: FDR (model checker), Casper (security protocol compiler), SatAbs (SAT-based model checker for C with predicate abstraction), CBMC (bounded model checker for C) and PRISM (probabilistic model checker). All are highly cited and widely used in industrial contexts, both for research and teaching. people Faculty AndrewKer | DanielKroening | MartaKwiatkowska | GavinLowe | TomMelham | LukeOng | JoelOuaknine | BillRoscoe | JamesWorrell Research PhilipArmstrong | DoinaBucur | Chris Chilton | AlastairDonaldson | MatthewHague | NannanHe | MarkKattenbelt | StefanKiefer | AndrzejMurawski | GethinNorman | DavidParker | HongyangQu | PhilippRuemmer | AshutoshTrivedi | ThomasWahl Students Sara Adams | PeterBoehm | ChristopherBroadbent | Chris Chilton | VijayD'Silva | LuFeng | MatthiasFruth | ChristophHaase | LeopoldHaller | ZiyadHanna | DavidHopkins | MarkJenkins | AlexanderKaiser | AllaaKamil | EricKerfoot | ManeeshKhattri | Tomasz Mazur | TobyMurray | LongNguyen | HristinaPalikareva | StevenRamsay | GeorgWeissenbacher | YongXie Administration JanetSadler info activities Concurrency | HardwareVerification | ModelChecking | PRISM | ProbabilisticModelChecking | ProbabilisticVerificationforSystemsBiology | QuantitativeAnalysisandVerification | Security | SoftwareModelChecking currentprojects AdvancedFormalVerificationTechniquesforHeterogeneousMulti-coreProgramming | AutomatedquantitativesoftwareverificationwithPRISM | AutomatedVerificationofProbabilisticPrograms | CESAR | CONNECT-IP | CSPModelChecking | EfficientVerificationofSoftwarewithReplicatedComponents | GAMES | GeneralisationOperatorsforAbstraction-Refinement | ModelCheckingPartiallyOrderedStateSpaces | ModelCheckingTimedSystemswithRestrictedResources:AlgorithmsandComplexity | Model-basedtestgenerationforembeddedsystems | Model-CheckingforTimedSystems | NewApproachestoSecurityandModelChecking | PredictableSoftwareSystems | PrivacyinOntology-BasedInformationSystems | QuantitativeVerification:FromModelCheckingtoModelMeasuring | TrustMetricsforSPKI/SDSI | UbiVal | VerificationofShared-MemoryConcurrentSoftware | VerifiedCommunicationProtocolsforMulticore/SoCArchitectures | VerifyingPropertiesoftheMLFamilyofLanguages completedprojects PushdownAutomataandGameSemantics | UbiquitousComputing The Computing Laboratory
信息来源于: The Computer Laboratory is the University of Cambridge's Computer Science department. Larry Paulson is made a Fellow of the ACM (2008) Larry Paulson has been made a Fellow of the ACM for his contributions to theorem provers and verification techniques. The ACM Fellows Program was established in 1993 to recognize and honour outstanding ACM members for their achievements in computer science and information technology and for their significant contributions to the mission of the ACM. The ACM Fellows serve as distinguished colleagues to whom the ACM and its members look for guidance and leadership as the world of information technology evolves. Larry is one of 44 distinguished computer scientists who will be inducted as Fellows of the ACM this year. The complete list can be found at http://fellows.acm.org/homepage.cfm . His research concerns mechanical theorem proving and its applications: continued development of the interactive theorem prover Isabelle applying automated theorem provers to verification problems applying set theory to specification and verification mechanizing selected areas of mathematics MetiTarski , an automatic prover for the elementary functions
标签: verification
