Abstract
The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.
Similar content being viewed by others
References
Lin H M. Complete inference systems for weak bisimulation equivalences in the π-calculus. Information and Computation, 2003, 180(1): 1–29
Lin H M, Wang Y. Axiomatising timed automata. Acta Informatica, 2002, 38(4): 277–305
Jiao L, Huang H J, Cheung T Y. Property-preserving composition by place merging. Journal of Circuits, Systems and Computers, 2005, 14(4): 793–812
Huang H J, Jiao L, Cheung T Y. Property-preserving subnet reductions for designing manufacturing systems with shared resources. Theoretical Computer Science, 2005, 332(1–3): 461–485
Jiao L, Cheung T Y, Lu WM. Handling synchronization problem in Petri-net-based system design by property-preserving transition-reduction. The Computer Journal, 2005, 48(6): 692–701
Jiao L, Cheung T Y. Compositional verification for workflow nets. Journal of Circuits, Systems and Computers, 2006, 15(4): 551–570
Zhang W H. Combining static analysis and case-based search space partitioning for reducing peak memory in model checking. Journal of Computer Science and Technology, 2003, 18(6): 762–770
Lv Y, Lin H M, Pan H. Computing invariants for parameter abstraction. In: Schneider K, Hoe J, eds. Proceedings of MEMOCODE. Nice: IEEE Press, 2007, 29–38
Wu P, Lin H M. Model-based testing of concurrent programs with predicate sequencing constrains. International Journal of Software Engineering and Knowledge Engineering, 2006, 16(5): 727–746
Lin H M. A predicate mu-calculus for mobile ambients. Journal of Computer Science and Technology, 2004, 20(1): 95–104
Lin H M. A predicate spatial logic and model checking for mobile processes. In: Liu Z M, Araki K, eds. Proceedings of ICTAC. Berlin: Springer, 2004, 36
Zhan N J, Majster-Cederbaum M. Deriving non-determinism from conjunction and disjunction. In: Wang F, ed. Proceedings of FORTE. Berlin: Springer, 2005, 351–365
Zhan N J, Wu J. Compositionality of fixpoint logic with chop. In: Hung D V, Wirsing M, eds. Proceedings of ICTAC. Berlin: Springer, 2005, 136–150
Zhang WH. Model checking with SAT-based characterization of ACTL formulas. In: Proceedings of ICFEM. Berlin: Springer, 2007, 191–211
Zhou C C, Hoare C A R, Ravn A. A calculus of durations. Information Processing Letters, 1991, 40(5): 269–276
Damm W, Hungar H, Olderog E-R. Verification of cooperating traffic agents. International Journal of Control, 2006, 79(5): 395–421
Zhou C C, Hansen MR. Duration calculus: a formal approach to real-time systems. EATCS Series of Monographs in Theoretical Computer Science. Berlin: Springer, 2004
Xu QW, Zhan N J. Formalizing scheduling theories with duration calculus. Nordic Journal of Computing, to appear
Liu C L, Layland J W. Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of ACM, 1973, 20(1): 46–61
Li GY, Tang Z S. Modeling real-time systems with continuous-time temporal logic. In: George C, Miao H, eds. Proceedings of ICFEM. Berlin: Springer, 2002, 231–236
Tang Z S. A program development support environment based on temporal logic. In: Proceedings of PLSD. North Hollland, 1983
Li GY, Tang Z S. Translating a continuous-time temporal logic into timed automata. In: Ohori A, ed. Proceedings of APLAS. Berlin: Springer, 2003, 322–338
Yan R J, Li G Y, Tang Z S. Symbolic model checking of finite precision timed automata. In: Hung D V, Wirsing M, eds. Proceedings of ICTAC. Berlin: Springer, 2005, 272–287
Fu Y, Wang H. Distributed utilization control for real-time clusters with load balancing. In: Proceedings of IEEE RTSS. Rio, 2006, 137–146
Zhou H, Wang Y J, Wang Q. Measuring internet bottlenecks: location, capacity, and available bandwidth. In: Lu XC, Zhao W, eds. Proceedings of CNMC. Berlin: Springer, 2005, 1052–1062
Wang X X, Wang Y J, Zhou J H, et al. Congestion control algorithm based on improved model in large-delay networks. Acta Electronica Sinica, 2005, 33(5): 842–846
Wang X L, Wang Y J, Zhou H, et al. PSO-PID: a novel controller for AQM routers. In: Proceedings of IEEE/IFIP WOCN. Bangalore, 2006, 1–5
Wang X L, Wang Y J, Zeng H T, et al. Particle swarm optimization with escape velocity. In: Proceedings of CIS. Guangzhou: IEEE Press, 2006, 457–460
Shen Y D, You J H, Yuan L Y, et al. A dynamic approach to characterizing termination of general logic programs. ACM Transactions on Computational Logic, 2003, 4(4): 417–430
Shen Y D, You J H, Yuan L Y. Enhancing global SLS-resolution with loop cutting and tabling mechanisms. Theoretical Computer Science, 2004, 328(3): 271–287
Dowek G, Jiang Y. Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theoretical Computer Science, 2006, 360(1–3): 193–208
Zhang WH, Huang Z, Zhang J. Parallel execution of stochastic search procedures on reduced SAT instances. In: Proceedings of PRICAI. Berlin: Springer, 2002, 108–117
Jia X X, Zhang J. Predicate-oriented isomorphism elimination in model finding. In: Proceedings of IJCAI. St Louis: Morgan Kaufmann Publishers, 2005, 1525–1526
Jia X X, Zhang J. A powerful technique to eliminate isomorphism in finite model search. In: Proceedings of IJCAR. Berlin: Springer, 2006, 318–331
Dong Y M. MLIRF method for specification acquisition and reuse. In: Proceedings of the 9th National Conference of China Computer Federation. Chongqing, 1996, 21–27 (in Chinese)
Dong YM. Recursive functions of context free languages (I) — the definitions of CFPRF and CFRF. Science in China Series F, 2002, 45(1): 25–39
Dong YM. Recursive functions of context free languages (II) — validity of CFPRF and CFRF definitions. Science in China Series F, 2002, 45(2): 1–21
Dong YM. An interactive learning algorithm for acquisition of concepts represented as CFL. Journal of Computer Science and Technology, 1998, 13(1): 1–8
Dong Y M, Li K, Chen H, et al. Design and implementation of the formal specification acquisition system SAQ. In: Proceedings of Conference Software: Theory and Practice, IFIP 16th World Computer Congress 2000. Beijing, 2000, 201–211
Sun J C. Multivariate fourier series over a class of non tensorproduct partition domains. Journal of Computational Mathematics, 2003, 21(1): 53–62
Sun J C, Yao J F. Fast generalized discrete fourier transforms on hexagon domains. Chinese Journal of Numerical Mathematics and Application, 2004, 26(3): 351–366
Sun J C, Li H Y. Generalized fourier transform on an arbitrary triangular domain. Advances in Computational Mathematics, 2005, 22: 223–248
Yao J F, Sun J C. HFFT on parallel dodecahedron domains and its parallel implementation. Numerical computation and computer applications, 2004, 4: 304–313 (in Chinese)
Sun J C. Multivariate fourier transform methods over simplex and super-simplex domains. Journal of Computational Mathematics, 2006, 24(3): 305–322
Zhang Y Q. Performance optimizations on parallel numerical software package and study on memory complexity. Dissertation for the Doctoral Degree. Beijing: Institute of Software, Chinese Academy of Sciences, 2000
Zhang Y Q. DRAM(h): a parallel computation model for high performance numerical computing. Chinese Journal of Computers, 2003, 26(12): 1660–1670
Zhang Y Q, Chen G L, Sun G Z, et al. Models of parallel computation: a survey and classification. Frontiers of Computer Science in China, 2007, 1(2): 156–165
Zhang Y Q, Sun J C, Tang Z M, et al. Memory complexity in high performance computing. In: Proceedings of HPC’ASIA. Singapore, 1998: 142–151
Alpern B, Carter L, Feig E, et al. The Uniform Memory Hierarchy Model of Computation. Algorithmica, 1994, 12(2–3): 72–109
Culler D, Karpy R, Patterson D, et al. LogP: towards a realistic model of parallel computation. In: Proceedings of PPoPP. San Diego, 1993, 1–12
Li M S. Expanding the horizons of software development processes: a 3-D integrated methodology. In: Proceedings of SPW. Beijing, 2005, 54–67
Li M S. Assessing 3-D integrated software development processes: a new benchmark. In: Proceedings of SPW/ProSim. Shanghai, 2006, 15–38
Wang Q, Li M S. Software process management: practices in China. In: Proceedings of SPW. Beijing, 2005, 317–331
Li M S. TRISO-model: a new approach to integrated software process assessment and improvement. Software Process: Improvement and Practice, 2007, 12(5): 387–398
Wang Q, Xiao J, Li M S, et al. A process-agent construction method for software process modeling in SoftPM. In: Proceedings of SPW/ProSim. Shanghai, 2006, 204–213
Li N, Li M S, Wang Q, et al. A negotiation model for the process agent in an agent-based process-centered software engineering environment. In: Proceedings of SEKE. San Francisco, 2006, 664–669
Zhao X, Chan K, Li M S. Applying agent technology to software process modeling and process-centered software engineering environment. In: Proceedings of SAC. Santa Fe, 2005, 1529–1533
Xiao J, Osterweil L J, Zhang L, et al. Applying little-JIL to describe process-agent knowledge in SoftPM. In: Proceedings of SPW/ProSim. Shanghai, 2006, 214–221
Zhang L, Wang Q, Xiao J, et al. A tool to create process-agents for OEC-SPM from historical project data. In: Proceedings of ICSP. Beilin: Springer, 2007, 84–95
Xiao J, Osterweil L J, Zhang L, et al. Applying little-JIL to describe process-agent knowledge and support project planning. Software Process: Improvement and Practice, 2007, 12(5): 437–448
Li MS, Yang Q, Zhai J, et al. On mobility of software processes. In: Proceedings of SPW/ProSim. Shanghai, 2006, 105–114
Yang Q, Li M S, Wang Q, et al. An algebraic approach for managing inconsistencies in software processes. In: Proceedings of ICSP. Berlin: Springer, 2007, 121–133
Yuan F, Li MS, Wan Z. SPEM2XPDL-towards SPEM model enactment. In: Proceedings of SERP. Las vegas, 2006, 240–245
Li J, Li M S, Wu Z, et al. A SPEM-based software process metamodel for CMM. Journal of Software, 2005, 16(8): 1366–1377
Yang D, Wan Y, Tang Z, et al. COCOMO-U: an extension of COCOMO II for cost estimation with uncertainty. In: Proceeding of SPW/ProSim. Shanghai, 2006, 132–141
Yang D, Boehm B, Yang Y, et al. Coping with the cone of uncertainty: an empirical study of the SAIV process model. In: Proceedings of ICSP. Berlin: Springer, 2007, 37–48
He M, Yang Y, Wang Q, et al. Cost estimation and analysis for government contract pricing in China. In: Proceedings of ICSP. Berlin: Springer, 2007, 134–146
Wang Q, Jiang N, Gou L, et al. BSR: a statistic-based approach for establishing and refining software process performance baseline. In: Proceedings of ICSE. Shanghai, 2006, 585–594
Wang Q, Li M S. Measuring and improving software process in China. In: Proceedings of ISESE. Noosa Heads, 2005, 183–192
Wang Q, Li M S, Liu X. An active measurement model for software process control and improvement. Journal of Software, 2005, 16(3): 407–418
Ruan L, Wang Y, Wang Q, et al. ARIMAmmse: an improved ARIMA-based software productivity prediction method. In: Proceedings of COMPSAC. Chicago, 2006, 17–21
Ruan L, Wang Y, Wang Q, et al. Empirical study on benchmarking software development tasks. In: the International Conference on Software Process. Minneapolis, 2007, 221–232
Zhang S, Wang Y, Yuan F, et al. Mining software repositories to understand the performance of individual developers. In: Proceedings of COMPSAC 2007. Beijing, 2007, 625–626
Zhang S, Wang Y, Tong J, et al. Evaluation of project quality: a DEA-based approach. In: Proceedings of SPW/ProSim. Shanghai, 2005, 88–96
Wang J, Li M S. A tridimensional requirements model and its support for stakeholder coordination. Journal of Software, 2007, 18(10): 2380–2392
Shu F, Zhao Y, Wang J, et al. User-driven requirements elicitation method with the support of personalized domain knowledge. Computer Research and Development, 2007, 44(6): 1044–1052
Huang M, Shu F, Li MS. A risk-driven method for prioritizing requirements in iteration development. Journal of Software, 2006, 17(12): 2450–2460
Li M S, Huang M, Shu F, et al. A risk-driven method for extreme programming release planning. In: Proceedings of ICSE 2006. Shanghai, 2006, 423–430
Huang T, Ding X N, Wei J. An application-semantics-based relaxed transaction model for internetware. Science in China Series F, 2006, 49(6): 774–791
Huang T, Chen N J, Wei J, et al. OnceAS/Q: a QoS-enabled web application server. Journal of Software, 2004, 15(12): 1787–1799
Chen H, Wu E H. An efficient radiosity solution for bump texture generation. Computer Graphics, 1990, 24(4): 125–134
Chen H, Wu E H. Radiosity for furry surfaces. In: Post F H, Barth W, eds. Proceedings of EUROGRAPHICS. North-Holland: Elsevier Science Publishers, 1991, 447–457
Wu E H. A radiosity solution for illumination of random fractal surfaces. The Journal of Visualization and Computer Animation, 1995, 6(4): 219–229
Chen Y Y, Sun H Q, Wu E H. Modeling and rendering snowy natural scenery using multi-mapping techniques. The Journal of Visualization and Computer Animation, 2003, 14(1): 21–30
Xu Y Q, Chen Y Y, Lin S, et al. Photo-realistic rendering of knitwear using the lumislice. In: Proceedings of ACM SIGGRAPH. New York: ACM Press, 2001, 391–398
Liu X H, Wu E H. Hierarchical structure with focus criterion for rendering height field. Journal of Computer Science and Technology, 1998, 13(12): 1–8
Wang W C, Wu E H. Adaptable splatting for irregular volume rendering. Computer Graphics Forum, 1999, 18(4): 213–222
Wang WC, Wu E H, Max N. A selective rendering method for data visualization. Journal of Visualization and Computer Animation, 1999, 10(3): 123–131
Wang W C, Zhou D H, Wu E H. Accelerating techniques in volume rendering of irregular data. Computers and Graphics, 1997, 21(3): 289–295
Wu E H, Liu Y Q, Liu X H. An improved study of real time fluid simulation on GPU (invited paper). Computer Animation and Virtual World, 2004, 15(3–4): 139–146
Liu Y Q, Liu X H, Wu E H. Real-time 3D fluid simulation on GPU with complex obstacles. In: Proceedings of Pacific Graphics. Seoul: IEEE Computer Society, 2004, 247–256
Liu Y Q, Liu X H, Wu E H. Fluid simulations on GPU with complex boundary conditions. In: Proceedings of Poster Workshop on GPGPU, at ACM SIGGRAPG, 2004
Liu Y Q, Zhu H B, Liu X H, et al. Real time simulation of physically based on-surface flow. The Visual Computer, 2005, 21(8–10): 727–734
Zhu H B, Liu X H, Liu Y Q, et al. Simulation of miscible binary mixtures based on lattice boltzmann method. Computer Animation and Virtual Worlds, 2006, 17(3–4): 403–411
Wu E H, Zhu H B, Liu X H, et al. Physically based fluid dynamics and interactions. In: Proceedings of CyberWorlds. Lausanne: IEEE Computer Society, 2006, 3–13
Fei GZ, Cai KY, Guo BN, et al. An adaptive sampling scheme for out-of-core simplification. Computer Graphics Forum, 2002, 21(2): 111–119
Wang W C, Li J, Wu E H. 2D point-in-polygon test by classifying edges into layers. Computers and Graphics, 2005, 29(3): 427–439
Wang WC, Li J, Sun HQ, et al. A layer-based representation of polyhedrons for point containment tests. IEEE Transactions on Visualization and Computer Graphics, 2007, to appear
Ao X, Wang XG, Tian F, et al. Cross-modal error correction of continuous handwriting recognition by Speech. In: Proceedings of ACM International Conference on Intelligent User Interfaces. Honolulu, 2007, 243–250
Ao X, Li J F, Wang X G, et al. Structuralizing digital ink for efficient selection. In: Proceedings of ACM International Conference on Intelligent User Interfaces. Sydney, 2006, 148–153
Li J F, Zhang X W, Ao X, et al. Sketch recognition with continuous feedback based on incremental intention extraction. In: Proceedings of ACM International Conference on Intelligent User Interfaces. San Diego, 2005, 145–150
Tian F, Ao X, Wang H A, et al. The tilt cursor: enhancing stimulus-response compatibility by providing 3D orientation cue of pen. In: ACM Conference on Human Factors in Computing Systems. San Jose, 2007, 303–306
Wang W X, Wang H, Dai G Z, et al. Visualization of large hierarchical data by circle packing. In: ACM Conference on Human Factors in Computing Systems. New York: ACM Press, 2006, 517–520
Xia M. Maximum edge-disjoint paths problem in planar graphs. In: Cai J Y, Cooper S B, Zhu H, eds. Proceedings of TAMC, 566–572
Zhang P. An approximation algorithm to the k-steiner forest problem. In: Cai J Y, Cooper S B, Zhu H, eds. Proceedings of TAMC, 2007, 728–737
Yan J, Zhang J. Backtracking algorithms and search heuristics to generate test suites for combinatorial testing. In: Proceedings of COMPSAC. Chicago: IEEE Computer Society, 2006, 385–394
Xu Z X, Zhang J. A test data generation tool for unit testing of C programs. In: Proceedings of QSIC, 2006, 107–116
Shen Y D, Zhang Z, Yang Q. Objective-oriented utility-based association mining. In: Proceedings of ICDM, 2002, 426–433
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Zhang, J., Zhang, W., Zhan, N. et al. Basic research in computer science and software engineering at SKLCS. Front. Comput. Sci. China 2, 1–11 (2008). https://doi.org/10.1007/s11704-008-0001-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11704-008-0001-3